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