Open xekoukou opened 7 years ago
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.
Trying to case split on
x
at the second case of thebelongs
function...gets me this error message: