Type inference for Nats breaks down

[RyanGlScott]

Another Practical Guide to Levitation–related bug. Here are some auxiliary definitions:

data Desc : Type -> Type where
  Ret : ix -> Desc ix
  Arg : (a : Type) -> (a -> Desc ix) -> Desc ix
  Rec : ix -> Desc ix -> Desc ix

Synthesise : Desc ix -> (ix -> Type) -> ix -> Type
Synthesise (Ret j)   x i = (j = i)
Synthesise (Rec j d) x i = (rec : x j ** Synthesise d x i)
Synthesise (Arg a d) x i = (arg : a   ** Synthesise (d arg) x i)

data Data : {ix : Type} -> Desc ix -> ix -> Type where
  Con :  {d : Desc ix} -> {i : ix}
      -> Synthesise d (Data d) i -> Data d i

CLabel : Type
CLabel = String

CEnum : Type
CEnum = List CLabel

VecCtors : CEnum
VecCtors = ["Nil", "Cons"]

data Tag : CLabel -> CEnum -> Type where
  TZ : Tag l (l :: e)
  TS : Tag l e -> Tag l (l' :: e)

SPi :  (e : CEnum)
    -> ((l : CLabel) -> Tag l e -> Type)
    -> Type
SPi []       _    = ()
SPi (l :: e) prop = (prop l TZ, SPi e $ \l' => \t => prop l' $ TS t)

switch :  (e : CEnum)
       -> (prop : (l : CLabel) -> (t : Tag l e) -> Type)
       -> SPi e prop
       -> (l' : CLabel) -> (t' : Tag l' e) -> prop l' t'
-- NB: Don't use the name "l'" for the first element of the CEnum, or you'll
-- trigger https://github.com/idris-lang/Idris-dev/issues/3651
switch (l :: e) prop (propz, props) l  TZ      = propz
switch (l :: e) prop (propz, props) l' (TS t') =
  switch e (\l => \t => prop l (TS t)) props l' t'

VecDesc : Type -> Desc Nat
VecDesc a =
  Arg CLabel $ \l =>
    Arg (Tag l VecCtors) $
      switch VecCtors (\_ => \_ => Desc Nat)
        ( Ret Z
        , ( Arg Nat $ \n => Arg a $ \_ => Rec n $ Ret $ S n
          , ()
          )
        ) l

Vec : (a : Type) -> Nat -> Type
Vec a n = Data (VecDesc a) n

If you try defining a Vec value like this, it typechecks:

exampleVecUgly : Vec Nat 3
exampleVecUgly = Con ("Cons" ** (TS TZ ** (2 ** (1 **
                  (Con ("Cons" ** (TS TZ ** (1 ** (2 **
                    (Con ("Cons" ** (TS TZ ** (0 ** 3 **
                      (Con ("Nil" ** (TZ ** Refl)) ** Refl)
                      )))) ** Refl)
                    )))) ** Refl)
                 )))

But if you try to abstract out the Nil and Cons operations like this:

Nil : {a : Type} -> Vec a Z
Nil = Con ("Nil" ** (TZ ** Refl))

Cons :  {a : Type} -> {n : Nat}
     -> a -> Vec a n -> Vec a (S n)
Cons {n} x xs = Con ("Cons" ** (TS TZ ** (n ** (x ** (xs ** Refl)))))

exampleVecIdeal : Vec Nat 3
exampleVecIdeal = Cons 1
                $ Cons 2
                $ Cons 3 Nil

Then exampleVecIdeal fails to typecheck!

Type checking ./Ch2_2.idr
Ch2_2.idr:77:17:
When checking right hand side of exampleVecIdeal with expected type
        Vec Nat 3

Type mismatch between
        Vec Integer 3 (Type of Cons 1 (Cons 2 (Cons 3 [])))
and
        Data (VecDesc Nat) (fromIntegerNat 3) (Expected type)

Specifically:
        Type mismatch between
                switch ["Nil", "Cons"]
                       (\underscore1, underscore2 => Desc Nat)
                       (Ret 0,
                        Arg Nat (\n => Arg Integer (\underscore => Rec n (Ret (S n)))),
                        ())
                       v0
        and
                switch ["Nil", "Cons"]
                       (\underscore1, underscore2 => Desc Nat)
                       (Ret 0,
                        Arg Nat (\n => Arg Nat (\underscore => Rec n (Ret (S n)))),
                        ())
                       v0

The workaround is to provide a type ascription on every single occurrence of Cons:

exampleVecWorkaround : Vec Nat 3
exampleVecWorkaround = Cons {a = Nat} 1
                     $ Cons {a = Nat} 2
                     $ Cons {a = Nat} 3 Nil

[ahmadsalim]

Thanks for the bug report.

I think the issue here is that Idris apparently does not detect that Cons and Nil are properly injective, and so does not try to nicely unify the type arguments. I would hope this would get fixed as well at some point.

[edwinb]

If anyone can point me at the appropriate rule for making this work, I'll improve the unification. As things stand, this is expected behaviour.

[edwinb]

(I can at least think of a way of making it work, I just don't know if it's the right one, or a properly general one, or... :))

[ahmadsalim]

@edwinb I think it could work if one only translated each numeral n to fromInteger n, instead of guessing the type of a numeral to be Integer too eagerly.