Unelaboratable syntactic form

[nicolabotta]

The program

> foo : {x, y : Double} -> EQ = compare x y -> So (x == y)
>   foo {x} {y} p | LT = ?kika

yields

- + Errors (1)
 `-- ./Double/open_issues/unelaboratable.lidr line 1 col 6:
     When checking type of Main.foo:
     When checking argument x to type constructor =:
             INTERNAL ERROR: Unelaboratable syntactic form So (Prelude.Interfaces.(==) {ty = _}
     {{%implementation}}
     x
     y)
     foo
     {x = x}
     {y = y}
     p | (|Prelude.Interfaces.LT , Prelude.Nat.LT , |)
             This is probably a bug, or a missing error message.
             Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

which I diligently report.

[ahmadsalim]

Thanks, it seems like it is missing some disambiguation when trying to typecheck LT. I think a with-clause is missing, so there should probably be an error regarding that.

[nicolabotta]

@ahmadsalim The code is crap, of course. The internal error disappears as soon as one reestablishes proper indentation:

> foo : {x, y : Double} -> EQ = compare x y -> So (x == y)
> foo {x} {y} p | LT = ?kika

yields

- + Errors (1)
 `-- ./Double/open_issues/unelaboratable.lidr line 1 col 6:
     When checking type of Main.foo:
     No such variable So

as one would expect. Notice, however, that in the indented version the type checker does a lot of work before exiting with the internal error reported in my original post. I do not think that this issue is relevant per se, just thought that the internal error could perhaps point at something that could be interesting in relation with more relevant issues.

[ahmadsalim]

@nicolabotta Yeah, thanks for reporting the error.