Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Implicit type variables don't seem to work when their types involve interface parameters

Open rntz opened this issue 1 year ago • 0 comments

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

rntz avatar Jul 14 '22 18:07 rntz