Zulip Chat Archive

Stream: general

Topic: Type error translating Agda to Lean 4


Sofia (Nov 20 2021 at 08:24):

Hello. I'm trying to translate the Desc type specified in Agda to Lean. I've translated the type, but I'm hitting a type error when translating the function operating over it.

https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/model/html/Chapter4.Desc.html

inductive Ty : Type (l + 1)
| var : Ty
| one : Ty
| prod (a b : Ty) : Ty
| sum (a b : Ty) : Ty
| sigma (S : Type l) (T : S -> Ty) : Ty
| pi (S : Type l) (T : S -> Ty) : Ty

namespace Ty
    universe a₁ a₂
    structure Lift (A : Type a₁) : Type (max a₁ a₂) where
        lower : A

    abbrev type : Ty -> Type l -> Type l
    | var, X => X
    | one, X => Lift Unit
    | prod a b, X => a.type X × b.type X
    | sum a b, X => a.type X  b.type X
    | sigma S T, X => Σ s : S, (T s).type X
    | pi S T, X => (s : S) -> (T s).type X
end Ty

Commenting out sigma and pi, everything is happy. Commenting out pi, shows sigma has an issue with universe levels. And commenting out sigma, shows pi has an issue with the recursion calls.

: error: stuck at solving universe constraint
  l =?= max l ?u.8093
while trying to unify
  Type l : Type (l + 1)
with
  Type (max ?u.8093 l) : Type (max (?u.8093 + 1) (l + 1))
structural recursion failed, produced type incorrect term
  application type mismatch
    match x✝¹, x : (x : Ty)  Type l  Ty.below (motive := fun x => Type l  Type l) x  Type l with
    | var, X => fun x => X
    | one, X => fun x => Lift Unit
    | prod a b, X => fun x => PProd.fst x.fst X × PProd.fst x.snd.fst X
    | sum a b, X => fun x => PProd.fst x.fst X  PProd.fst x.snd.fst X
    | pi S T, X => fun x => (s : S)  PProd.fst x.fst s X
  argument has type
    (S : Type u_1)  (T : S  Ty)  Type l  Ty.below (motive := fun x => Type l  Type l) (pi S T)  Type (max u_1 l)
  but function has type
    ((S : Type u_1) 
        (T : S  Ty) 
          (X : Type l)  (fun x x_1 => Ty.below (motive := fun x => Type l  Type l) x  Type l) (pi S T) X) 
      (fun x x_1 => Ty.below (motive := fun x => Type l  Type l) x  Type l) x✝¹ x

'termination_by' modifier missing

(And again with partial on the abbreviation, to simplify the error.)

: error: application type mismatch
  match x✝¹, x with
  | var, X => X
  | one, X => Lift Unit
  | prod a b, X => type._unsafe_rec a X × type._unsafe_rec b X
  | sum a b, X => type._unsafe_rec a X  type._unsafe_rec b X
  | pi S T, X => (s : S)  type._unsafe_rec (T s) X
argument has type
  (S : Type u_1)  (S  Ty)  Type l  Type (max u_1 l)
but function has type
  ((S : Type u_1)  (T : S  Ty)  (X : Type l)  (fun x x => Type l) (pi S T) X)  (fun x x => Type l) x✝¹ x

Sofia (Nov 20 2021 at 08:43):

Simplifying the error in the second case we have:

Function argument:
(S : Type u_1)  (S  Ty)  Type l  Type l

Called with:
(S : Type u_1)  (S  Ty)  Type l  Type (max u_1 l)

Mario Carneiro (Nov 20 2021 at 08:51):

aside: You shouldn't use abbrev for definitions by pattern matching

Mario Carneiro (Nov 20 2021 at 08:52):

at least, I don't think it works the way you want

Sofia (Nov 20 2021 at 08:53):

I forgot the inline / reducible annotation and used that to let Lean reduce it when it needed to.

Mario Carneiro (Nov 20 2021 at 08:53):

lean will always reduce it when it needs to

Mario Carneiro (Nov 20 2021 at 08:54):

def is not opaque

Mario Carneiro (Nov 20 2021 at 08:54):

To answer your actual question, you need Ty.{l} in the type signature of type

Sofia (Nov 20 2021 at 08:55):

I do know using abbrev or @[reducible] has been necessary for some of my code where just def didn't work.

Sofia (Nov 20 2021 at 08:55):

Ahuh! That is the syntax to bind it there..... Couldn't find it in docs...

Mario Carneiro (Nov 20 2021 at 08:55):

in most cases, you should be using simp or unfold or such to unfold a definition only when necessary

Mario Carneiro (Nov 20 2021 at 08:56):

unfolding eagerly is really bad for lean, it can cause the terms to get out of control if you use it too much

Sofia (Nov 20 2021 at 08:57):

Noted.

Sofia (Nov 20 2021 at 08:58):

Thanks for the Ty.{l} detail. :)

Sofia (Nov 20 2021 at 09:01):

I'll see if I "need" the abbrev hack and revisit that issue. :)


Last updated: Dec 20 2023 at 11:08 UTC