Why does Idris 2 fail to resolve constraints with function composition in this trivial example?

Question

I have encountered a problem with some code I am trying to write in Idris 2. I would like to resolve this issue, but more importantly, I wish to understand it more deeply and develop some skills in diagnosing such issues in general.

I have distilled the problem to the following relatively trivial example:

data D : Nat -> Type where
  V : (n : Nat) -> D n

d : (n : Nat) -> D n
d n = V n

f : D n -> String
f (V n) = show n

t : Nat -> String
t = f . d

The definition of t fails type checking with the following output:

Error: While processing right hand side of t. Can't solve constraint between: ?n [no locals in scope] and n.

Test:11:9--11:10
 07 | f : D n -> String
 08 | f (V n) = show n
 09 | 
 10 | t : Nat -> String
 11 | t = f . d

Some experimentation has revealed that the following alternative definitions for t also fail type checking:

t : Nat -> String
t n = (f . d) n

t : Nat -> String
t = \n => (f . d) n

While these alternatives type check successfully:

t : Nat -> String
t n = f (d n)

t : Nat -> String
t = \n => f (d n)

I am endeavouring to learn Idris (for the second time), and so while I could move on with the definitions which don't involve function composition, I would like to improve my understanding.

It seems to me that the definitions which pass type checking are simply syntactic alternatives with identical semantics and behaviour, and I don't understand why the function composition definitions fail type checking. I would also like to understand the particular error message the type checker reports, so that I can deepen my understanding and resolve similar type checking errors in the future.

I have a few broad questions:

• How should I interpret the error reported by the type checker in this example, and how can I gather more information about the ?n and n types mentioned? I particularly welcome any advice or tips on how to go about understanding and resolving such an error (teach a man to fish, as the saying goes).
• Why do the definitions involving function composition fail type checking?
• What is the best solution for this example? Should I just use a definition which does not involve function composition? Is there a better alternative?

Answer 1

Let look at the types involved

Prelude.. : (b   -> c     ) -> (a        -> b   ) -> a -> c
f :          D n -> String
d :                             (n : Nat) -> D n

The problem is:

(a        -> b   )
(n : Nat) -> D n

cannot be unified because (a -> b) does not allow the value of the argument to determine the type of return value.