Compiler failed to unify Type -> Type

[iacore]

Steps to Reproduce

data Foo : Type -> Type where
   MkFoo : Foo a

data F : (Type -> Type) -> Type where
   MkF : v a -> F v

ans : ()
ans = do
   let f = MkF MkFoo
   ?help

Expected Behavior

The code should type check.

Observed Behavior

1/1: Building match (match.idr)
Error: While processing right hand side
of ans. Can't solve constraint
between: Foo a and ?v ?a.

match:14:16--14:21
 10 |    MkT : {v: _} -> v a -> T a
 11 | 
 12 | ans : ()
 13 | ans = do
 14 |    let f = MkF MkFoo
                     ^^^^^

[iacore]

Attempt 2

match_me : f t -> Eff [f] t
match_me x = MkEff x

ans : Eff [Foo] ()
ans = do
   let interim = match_me MkFoo
   ?help

Observed behavior

1/1: Building match (match.idr)
Error: While processing right hand side
of ans. Can't solve constraint
between: Foo a and ?f ?t.

match:17:27--17:32
 13 | -- foo = MkFoo
 14 | 
 15 | ans : Eff [Foo] ()
 16 | ans = do
 17 |    let interim = match_me MkFoo
                                ^^^^^

Error(s) building file match.idr
Main> :t help
   interim : Eff [?f] ?t
------------------------------
help : Eff [Foo] ()

[buzden]

The signature of your match_me looks inappropriate for the purpose, you are using it for. Why do you use auto-implicit argument instead of just implicit argument? auto-implicit arguments are such arguments which value compiler should search for based entirely on its type. In your case, the value of the argument should be found from other arguments. So, usual implicit argument should be used.

I.e., if you change the signature to

match_me : (f: Type -> Type) => f t -> Eff [f] t

or even to

match_me : f t -> Eff [f] t

your original code typechecks.

UPD: My answer is the answer only to the original issue, I didn't see your attempt 2, where you use usual implicit argument.

In the attempt 2 the type of interim is still ambiguous on a, so behaviour is not terribly suprising, but why something like this

ans = do
   let ff : Foo Nat = MkFoo
   let interim = match_me ff
   ?help

causes While processing right hand side of ans. Can't solve constraint between: Foo Nat and ?f ?t -- well, I don't know, it could be matched, I think.

[iacore]

maybe Idris cannot unify higher-ordered type like Foo Nat?

[gallais]

Did you mean to have MkEff : Elem v vs => v a -> Eff vs a? In your code you have v s -> Eff vs a which means there is no connection whatsoever between the index a and the argument s to v.

[iacore]

Sorry, typo. Attempt 2 still produce the same error.

[gallais]

Attempt 2 does not have an input type coming in. For all idris knows, f = id, t = Foo a is valid.

[iacore]

Is there a work around? It seem to be one fundamental behavior of Idris.

[gallais]

• Give a type annotation to interim.
• Or use it in a context that provides enough information that the f can be uniquely reconstructed.
• Or explicitly pass the argument match_me {f = Foo}

[iacore]

Should I close this issue? Or maybe the error message could be better?

This behaviour stopped me from making do notation more flexible:

https://github.com/locriacyber/idris2-eff/blob/0403d8128b0b1fa21cb315dc0d99bbd9239a8ff0/src/Control/Eff/Sugar.idr#L10-L13 https://github.com/locriacyber/idris2-eff/blob/0403d8128b0b1fa21cb315dc0d99bbd9239a8ff0/src/Test/Sugar.idr