The compiler seems to struggle to unify interfaces with dependent types with their implementation.
Steps to Reproduce
try to compile this module:
module Test
data Dummy : (lbl : Type) -> (st : List lbl) -> Type -> Type where
MkDummy : a -> Dummy b st a
public export
interface IxPure (f : (lbl : Type) -> (st : List lbl) -> Type -> Type)
where
ixPure : a -> f lbl st a
IxPure Dummy where
ixPure = MkDummy
pure12 : Dummy String xs Integer
pure12 = ixPure $ 12
Fails with:
Expected Behavior
It should compile.
Observed Behavior
It fails with:
Test.idr:16:10--17:1:While processing right hand side of pure12 at Test.idr:16:1--17:1:
Can't find an implementation for IxPure ?f
Workarounds
Specifying explicitly the value of f in pure12 solve the issue:
The compiler seems to struggle to unify interfaces with dependent types with their implementation.
Steps to Reproduce
try to compile this module:
Fails with:
Expected Behavior
It should compile.
Observed Behavior
It fails with:
Workarounds
Specifying explicitly the value of
f
inpure12
solve the issue:And the problem disappears as well if we remove the
st
parameters.