Misterious type mismatch error: line 0 col -1

[nicolabotta]

The program

> module issues.type_mismatch

> %default total
> %access public export
> %auto_implicits off

> M        : Type -> Type
> fmap     : {A, B : Type} -> (A -> B) -> (M A -> M B)
> ret      : {A : Type} -> A -> M A
> bind     : {A, B : Type} -> M A -> (A -> M B) -> M B
> Elem     : {A : Type} -> A -> M A -> Type
> NotEmpty : {A : Type} -> M A -> Type
> All      : {A : Type} -> (P : A -> Type) -> M A -> Type
> tagElem  : {A : Type} -> (ma : M A) -> M (DPair A (\ a => a `Elem` ma))
> allElemS : {A : Type} -> {P : A -> Type} ->
>            (a : A) -> (ma : M A) -> All P ma -> a `Elem` ma -> P a

> Foo : (t : Nat) -> Type
> Bar : (t : Nat) -> (x : Foo t) -> Type
> foo : (t : Nat) -> (x : Foo t) -> (y : Bar t x) -> M (Foo (S t))

> Open : {t : Nat} -> (n : Nat) -> Foo t -> Type

> Good : (t : Nat) -> (x : Foo t) -> (n : Nat) -> (Bar t x) -> Type
> Good t x n y = (NotEmpty (foo t x y), All (Open {t = S t} n) (foo t x y))

> GoodBar : (t : Nat) -> (x : Foo t) -> (n : Nat) -> Type
> GoodBar t x n = DPair (Bar t x) (Good t x n)

> allOpen : {t, n : Nat} -> {x : Foo t} -> (y : GoodBar t x n) -> All (Open n) (foo t x (fst y)) 
> allOpen (MkDPair _ p) = snd p

> Pol : (t : Nat) -> (n : Nat) -> Type
> Pol t  Z    = Unit
> Pol t (S m) = (x : Foo t) -> Open (S m) x -> GoodBar t x m

> data PolSeq : (t : Nat) -> (n : Nat) -> Type where
>   MkNilPolSeq : {t : Nat} -> PolSeq t Z
>   (::)        : {t, n : Nat} -> Pol t (S n) -> PolSeq (S t) n -> PolSeq t (S n)

> data FooBarSeq : (t : Nat) -> (n : Nat) -> Type where
>   MkNilFooBarSeq : {t : Nat} -> (x : Foo t) -> FooBarSeq t Z
>   (++)           : {t, n : Nat} -> DPair (Foo t) (Bar t) -> FooBarSeq (S t) n -> FooBarSeq t (S n)

> run : {t, n : Nat} -> 
>       (x : Foo t) -> (v : Open n x) ->
>       (ps : PolSeq t n) ->
>       (eps : {A : Type} -> M A -> A) ->
>       FooBarSeq t n
> run {t} {n = Z}    x v MkNilPolSeq eps = MkNilFooBarSeq x
> run {t} {n = S m}  x v (p :: ps') eps =
>   (MkDPair x y) ++ (eps (fmap f (tagElem mx'))) where
>     y   : Bar t x
>     y   = fst (p x v)
>     mx' : M (Foo (S t))
>     mx' = foo t x y
>     av  : All (Open m) mx'
>     av  = allOpen (p x v)
>     f   : DPair (Foo (S t)) (\ x' => x' `Elem` mx') -> FooBarSeq (S t) m
>     f (MkDPair x' x'emx') = run x' v' ps' eps where
>       v' : Open m x'
>       v' = allElemS x' mx' av x'emx'

fails to type check with

- + Errors (1)
 `-- (val) line 0 col -1:
     When checking type of issues.type_mismatch.run, f, v':
     Type mismatch between
             Type
     and
             M _

The error seems to suggest that this is not the expected behavior.

[ahmadsalim]

I can see that the error location is wrong, but the error should be around the definition of v' in the where block of f, in the where block of run.

[ahmadsalim]

It seems that Open is not defined, so I am actually unsure whether this should type check. I however agree that the error message could be better.

[nicolabotta]

@ahmadsalim What would be the problem with Open not being defined? M, fmap, ret, bind, Elem, NotEmpty, All, tagElem, allElemS, Foo, Bar and foo are also not defined. Generally speaking, the type checker seems to work better with undefined values than with defined ones, because of #172, #761, #2837, #3246. Perhaps we have here a counterexample?

[nicolabotta]

@ahmadsalim "I can see that the error location is wrong, but the error should be around the definition of v' in the where block of f, in the where block of run.": the problem is that

>     f (MkDPair x' x'emx') = run x' v' ps' eps where
>       v' : Open m x'
>       v' = ?kika -- allElemS x' mx' av x'emx'

does not type check with the same error message. At the same time,

>     f (MkDPair x' x'emx') = run x' ?v' ps' eps -- where
>       -- v' : Open m x'
>       -- v' = ?kika -- allElemS x' mx' av x'emx'

type checks fine and the type of the ?v' goal is reported to be Open m x'. This makes me suspect that there is something wrong with the Idris type checker.

[ahmadsalim]

@nicolabotta Perhaps, I misunderstood, but I had believed that the Idris type checker required definitions of functions used in types in order to type check (because it may depend on their reduction semantics). By all means I am not an expert in the details of the implementation, and if it does work without in other cases, then maybe the error lies somewhere else.

[nicolabotta]

@ahmadsalim I am not an expert either, of course. But the type checker seems to be fine with the computation of av that also depends on Open. My guess ist that the culprit here is actually eps. We know that Idris has sometimes troubles with dependently typed higher order functions. Also, notice that

> bar : {t, n : Nat} -> (x : Foo t) -> (v : Open n x) ->
>       (ps : PolSeq t n) -> M (FooBarSeq t n)
> bar {t} {n = Z}    x v MkNilPolSeq =  ret (MkNilFooBarSeq x)
> bar {t} {n = S m}  x v (p :: ps')  =
>   fmap g (bind (tagElem mx') f) where
>     y   :  Bar t x
>     y   =  fst (p x v)
>     mx' :  M (Foo (S t))
>     mx' =  foo t x y
>     av  :  All (Open m) mx'
>     av  =  allOpen (p x v)
>     g   :  FooBarSeq (S t) m -> FooBarSeq t (S m)
>     g   =  ((MkDPair x y) ++)
>     f   :  DPair (Foo (S t)) (\ x' => x' `Elem` mx') -> M (FooBarSeq (S t) m)
>     f (MkDPair x' x'emx') = bar {n = m} x' v' ps' where
>       v'  :  Open m x'
>       v'  =  allElemS x' mx' av x'emx'

type checks fine and the main difference between run and bar is that the latter does not depend on an argument of type {A : Type} -> M A -> A. Therefore my conjecture is that eps makes a weakness of the type checker (or of the error reporting machinery) visible.

[nicolabotta]

As it turns out, this

> eps : {A : Type} -> M A -> A

> run : {t, n : Nat} -> 
>       (x : Foo t) -> (v : Open n x) ->
>       (ps : PolSeq t n) ->
>       FooBarSeq t n
> run {t} {n = Z}    x v MkNilPolSeq = MkNilFooBarSeq x
> run {t} {n = S m}  x v (p :: ps')  =
>   (MkDPair x y) ++ (eps (fmap f (tagElem mx'))) where
>     y   : Bar t x
>     y   = fst (p x v)
>     mx' : M (Foo (S t))
>     mx' = foo t x y
>     av  : All (Open m) mx'
>     av  = allOpen (p x v)
>     f   : DPair (Foo (S t)) (\ x' => x' `Elem` mx') -> FooBarSeq (S t) m
>     f (MkDPair x' x'emx') = run x' v' ps' where
>       v' : Open m x'
>       v' = allElemS x' mx' av x'emx'

Thus, there seems to be a problem in Idris with type dependent high order functions.