type mismatch between m and (minus m 0)

Question

I'm trying to define the dependent type of n-ary functions (built as a tree out of binary and unary functions; I suspect this is isomorphic to the type of (Vect n a) -> a) as an exercise in learning Idris.

While trying to define a function that applies an argument to an n-ary function (producing an (n-1)-ary function) I got a very suspicious error:

    Type mismatch between
            ArityFn m a (Type of ng)
    and
            ArityFn (minus m 0) a (Expected type)

    Specifically:
            Type mismatch between
                    m
            and
                    minus m 0

here's the code in question, for reference

data ArityFn : Nat -> (ty: Type) -> Type where
  Val       : (x : ty) -> ArityFn 0 ty
  UnaryFn   : (ty -> ty) -> ArityFn 1 ty
  BinaryFn  : (ty -> ty -> ty) -> ArityFn 2 ty
  NAryFn    : (ty -> ty -> ty) -> (ArityFn n ty) -> (ArityFn m ty) -> ArityFn (n + m) ty

%name ArityFn nf, ng, nh

applyArityFn : a -> (ArityFn n a) -> (LTE 1 n) -> ArityFn (n - 1) a
 ... (some definitions elided)
applyArityFn x (NAryFn h (UnaryFn f)  ng) _ = mkNAryFn h (Val (f x))     ng

is this a bug in the typechecker?

Answer 1

When in doubt, look for the definition of the function which got stuck:

:def minus returns (among other things, modulo some cleanup):

Original definiton:
minus 0 right = 0
minus left 0 = left
minus (S left) (S right) = minus left right

You can see that minus left 0 = left won't hold definitionally because there is a pattern minus 0 right = 0 before. Now, of course both equations return the same result when they happen to coincide but idris doesn't know that.

To get the result you want you can:

• either somehow pattern match on m and get minus to reduce now that the head constructor of its first argument is exposed
• or rewrite by a proof that minus m 0 = m.