Idris2
Idris2 copied to clipboard
Implicit type variables don't seem to work when their types involve interface parameters
With Idris 2, version 0.5.1-68a144bf1. The following code:
interface Cat obj (hom: obj -> obj -> Type) where
id : hom a a
produces the error:
While processing type of id. Can't solve constraint between: ?type_of_a [no locals in scope] and obj.
error:2:12--2:13
1 | interface Cat obj (hom: obj -> obj -> Type) where
2 | id : hom a a
If we change this to add an explicit implicit argument, it works:
interface Cat obj (hom: obj -> obj -> Type) where
id : {0 a: obj} -> hom a a