Case splitting results in error message "Elaborating Builtins.Pair arg A: CantUnify False ....."

[xekoukou]

Trying to case split on x at the second case of the belongs function...

import Data.Vect

data Node : String -> Type where
  MkNode : (s : String) -> Node s

belongs : ((s : String ** Node s), Nat) -> Vect n ((s : String ** Node s), Nat) -> Bool
belongs x [] = False
belongs x (y :: xs) = ?belongs_rhs_2

gets me this error message:

(val):Elaborating Builtins.Pair arg A: CantUnify False (Builtins.DPair {a1016} {P1017},Just (SourceTerm Builtins.MkDPair {a1016} {P1017} {x1018} {pf1019})) and (Type 0,Just ExpectedType) CantUnify False (Builtins.DPair {a1016} {P1017},Nothing) and (Type 0,Nothing)  in [({p
f1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> Type 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0 in [({pf1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> T
ype 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0

[LeifW]

I think https://github.com/idris-lang/Idris-dev might be a more appropriate place to report this issue, as that message is coming from Idris, and there's nothing the vim mode can do about it.

When I load that code in the repl, and then run the command :casesplit 8 x (assuming that second case you're splitting is on line 8 of the file), I get:

(val):When checking argument A to type constructor Builtins.Pair:
        Type mismatch between
                DPair a P (Type of (x ** pf))
        and
                Type (Expected type)
Holes: Main.belongs_rhs_2

That's essentially what the vim case split command is doing; however, when you replicate the mechanism it uses to talk to the repl, by running the following from the command line: idris --client ':l Foo.idr' (assuming your file is Foo.idr), and then idris --client ':cs 8 x', you get the message you reported:

(val):Elaborating Builtins.Pair arg A: CantUnify False (Builtins.DPair {a1016} {P1017},Just (SourceTerm Builtins.MkDPair {a1016} {P1017} {x1018} {pf1019})) and (Type 0,Just ExpectedType) CantUnify False (Builtins.DPair {a1016} {P1017},Nothing) and (Type 0,Nothing)  in [({pf1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> Type 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0 in [({pf1019},{P1017} {x1018}),({x1018},{a1016}),({P1017},{a1016} -> Type 0),({a1016},Type 0),(x,Builtins.Pair (Builtins.DPair String (\ s : String => Main.Node s)) Prelude.Nat.Nat),({k509},Prelude.Nat.Nat)] 0

Not sure why it's so different than what you see directly at the REPL.