Zulip Chat Archive
Stream: new members
Topic: non valid occurrence
Quinn (Mar 22 2024 at 20:07):
what does
(kernel) arg #7 of 'TypeExp.type_op' contains a non valid occurrence of the datatypes being declared
mean if the constructor in question only has 5 arguments?
Timo Carlin-Burns (Mar 22 2024 at 20:19):
I don't know without seeing any code. Mind providing a #mwe?
Quinn (Mar 22 2024 at 20:22):
i don't think I understand this enough to provide a minimal working example! but here's the code)
Kyle Miller (Mar 22 2024 at 20:23):
"minimal" is an aspiration, any working example after deleting irrelevant stuff is good
Quinn (Mar 22 2024 at 20:23):
Kyle Miller (Mar 22 2024 at 20:23):
Zulip hint: #backticks
Kyle Miller (Mar 22 2024 at 20:24):
Code blocks with backticks also give a link to the live editor, and even better you can see the code right here
Quinn (Mar 22 2024 at 20:24):
didn't know that about the link to the live editor!
Quinn (Mar 22 2024 at 20:24):
variable [Decidable Asset] {Asset : Type}
variable [Decidable Party] {Party : Type}
inductive Var : Type :=
| V1
| VS (v : Var)
inductive ObsLabel : Type :=
| LabelReal (o : String)
| LabelBool (o : String)
inductive Op : Type :=
| Add
| Sub
| Mult
| Div
| And
| Or
| Less
| Leq
| Eq
| Not
| Neg
| BLiteral (b : Bool)
| RLiteral (r : Int)
| Cond
inductive Exp : Type :=
| OpE (op: Op) (args : List Exp) : Exp
| Obs (l : ObsLabel) (i : Int) : Exp
| VarE (v : Var) : Exp
| Acc (f : Exp) (d : Nat) (e : Exp) : Exp
inductive Contract : Type :=
| Zero : Contract
| Let : Exp -> Contract -> Contract
| Transfer : Party -> Party -> Asset -> Contract
| Scale : Exp -> Contract -> Contract
| Both : Contract -> Contract -> Contract
| If : Exp -> Contract -> Contract -> Contract
inductive Ty : Type :=
| REAL
| BOOL
inductive TypeOp : Op -> List Ty -> Ty -> Prop :=
| type_blit b : TypeOp (Op.BLiteral b) [] BOOL
| type_rlit r : TypeOp (Op.RLiteral r) [] REAL
| type_neg : TypeOp Op.Neg [REAL] REAL
| type_not : TypeOp Op.Not [BOOL] BOOL
| type_cond t : TypeOp Op.Cond [BOOL,t,t] t
| type_add : TypeOp Op.Add [REAL,REAL] REAL
| type_sub : TypeOp Op.Sub [REAL,REAL] REAL
| type_mult : TypeOp Op.Mult [REAL,REAL] REAL
| type_div : TypeOp Op.Div [REAL,REAL] REAL
| type_and : TypeOp Op.And [BOOL,BOOL] BOOL
| type_or : TypeOp Op.Or [BOOL,BOOL] BOOL
| type_less : TypeOp Op.Less [REAL,REAL] BOOL
| type_leq : TypeOp Op.Leq [REAL,REAL] BOOL
| type_eq : TypeOp Op.Eq [REAL,REAL] BOOL
notation "|-Op" e ":" t "=>" r => TypeOp e t r
inductive TypeObs : ObsLabel -> Ty -> Prop :=
| type_obs_bool b : TypeObs (ObsLabel.LabelBool b) BOOL
| type_obs_real r : TypeObs (ObsLabel.LabelReal r) REAL
notation "|-O" e ":" t => TypeObs e t
def TyEnv := List Ty
inductive TypeVar : TyEnv -> Var -> Ty -> Prop :=
| type_var_1 t g : TypeVar (t::g) Var.V1 t
| type_var_S g v t t' : TypeVar g v t -> TypeVar (t'::g) (Var.VS v) t
notation g "|-X" v ":" t => TypeVar g v t
def List.all2 {A B} (P : A -> B -> Prop) : List A -> List B -> Prop
| [], [] => True
| a::as, b::bs => P a b /\ List.all2 P as bs
| _, _ => False
inductive TypeExp : TyEnv -> Exp -> Ty -> Prop :=
| type_op g op es ts (t : Ty) : (|-Op op : ts => t) -> List.all2 (TypeExp g) es ts -> TypeExp g (Exp.OpE op es) t
| type_obs (t : Ty) g o z : (|-O o : t) -> TypeExp g (Exp.Obs o z) t
| type_var t g v : (g |-X v : t) -> TypeExp g (Exp.VarE v) t
| type_acc n t g e1 e2 : ((t::g) |-X Var.V1 : t) -> TypeExp g e1 t -> TypeExp g e2 t -> TypeExp g (Exp.Acc e1 n e2) t
Quinn (Mar 22 2024 at 20:24):
i'm not sure what's irrelevant, cuz it's cumulative
Kyle Miller (Mar 22 2024 at 20:24):
(check out the two icons in the upper right corner of the code block. "Lean 4 Playground" goes to the online editor)
Quinn (Mar 22 2024 at 20:24):
it's TypeExp that has the bug, which uses everything that came before.
Timo Carlin-Burns (Mar 22 2024 at 20:27):
arg #7 of 'TypeExp.type_op' in the error is referring to the hypothesis List.all2 (TypeExp g) es ts
Quinn (Mar 22 2024 at 20:28):
oh. I find that confusing
Quinn (Mar 22 2024 at 20:28):
nvm. I thought about it more---- premises after the : are equivalent to arguments, in inductive constructors.
Quinn (Mar 22 2024 at 20:31):
Thank you
Quinn (Mar 22 2024 at 20:32):
i'm noticing i'm allowed to treat a partially applied type as the function that gets passed into all2.
#check List.all2 (TypeVar g) [Var.V1, Var.VS Var.V1] [Ty.REAL, Ty.REAL]
(valid Prop), but maybe it doesn't want me to do so in an input to a constructor
Mario Carneiro (Mar 22 2024 at 20:35):
Yes, constructors are limited in the kinds of positions you can have the type under definition appearing
Timo Carlin-Burns (Mar 22 2024 at 20:35):
Here is a possible alternative
inductive TypeExp : TyEnv -> Exp -> Ty -> Prop :=
| type_op g op es ts (t : Ty) : (|-Op op : ts => t) -> (∀ p ∈ List.zip es ts, TypeExp g p.1 p.2) -> TypeExp g (Exp.OpE op es) t
| type_obs (t : Ty) g o z : (|-O o : t) -> TypeExp g (Exp.Obs o z) t
| type_var t g v : (g |-X v : t) -> TypeExp g (Exp.VarE v) t
| type_acc n t g e1 e2 : ((t::g) |-X Var.V1 : t) -> TypeExp g e1 t -> TypeExp g e2 t -> TypeExp g (Exp.Acc e1 n e2) t
Mario Carneiro (Mar 22 2024 at 20:36):
if you use zip you will want to say the lengths are equal on the side
Mario Carneiro (Mar 22 2024 at 20:36):
but this will indeed work as an alternative
Quinn (Mar 22 2024 at 20:37):
Yes, constructors are limited in the kinds of positions you can have the type under definition appearing
is this different from coq? I remember about strictly positive occurrences but i didn't think that meant I can't have a conjunction
Mario Carneiro (Mar 22 2024 at 20:37):
the fundamental rules are not different, but Coq is significantly more aggressive about recursing into definitions and other inductives to justify that the use of the type under definition is positive
Quinn (Mar 22 2024 at 20:38):
I see! So can I mark my List.all2 function as "unfold this at the slightest provocation"?
Mario Carneiro (Mar 22 2024 at 20:39):
with lean it's a much more syntactic check: it has to be at the end of a forall expression (as in Timo's code) and cannot be as an argument to other functions
Mario Carneiro (Mar 22 2024 at 20:39):
that won't work here because you can't unfold all2 in this position
Mario Carneiro (Mar 22 2024 at 20:40):
You can define this as a mutual inductive type, this is the closest thing to what lean would do with your definition if it was smart enough
Quinn (Mar 22 2024 at 20:40):
That makes sense!
Mario Carneiro (Mar 22 2024 at 20:42):
BTW your variable declarations are backwards:
variable [Decidable Asset] {Asset : Type}
variable [Decidable Party] {Party : Type}
Quinn (Mar 22 2024 at 20:46):
side question: what's going on wiht forall item \in xs for list xs? I'm not familiar with that, and neither is my lean4 session. I had to do forall p, p \in List.zip es ts -> TypeExp g p.1 p.2 instead
Timo Carlin-Burns (Mar 22 2024 at 20:48):
it's syntax sugar for exactly what you wrote. I believe it was moved from Std to Init in a recent version of Lean, so you might need to import Std to get the notation
Quinn (Mar 22 2024 at 20:48):
variable [Decidable Asset] {Asset : Type}
what's the correct way?
Timo Carlin-Burns (Mar 22 2024 at 20:49):
variable {Asset : Type} [Decidable Asset]
Quinn (Mar 22 2024 at 20:50):
Huh. flipping it that way gives me
Messages here (1)
1:35:
application type mismatch
Decidable Asset
argument
Asset
has type
Type : Type 1
but is expected to have type
Prop : Type
Mario Carneiro (Mar 22 2024 at 20:50):
that's because types can't be Decidable
Mario Carneiro (Mar 22 2024 at 20:50):
maybe you meant DecidableEq?
Quinn (Mar 22 2024 at 20:51):
ah--- yeah that's what I wanted
Timo Carlin-Burns (Mar 22 2024 at 20:51):
in your version you were referencing Asset before declaring it and so it was getting inserted as an auto-implicit variable of type Prop. Then you additionally declared a second variable Asset : Type
Quinn (Mar 22 2024 at 20:51):
I really only need equality to be decidable
Quinn (Mar 22 2024 at 20:51):
oh that's confusing! so there can be shadowed implicits
Timo Carlin-Burns (Mar 22 2024 at 20:52):
I often add set_option autoImplicit false to the top of my files to avoid these accidents
Quinn (Mar 22 2024 at 20:55):
this is great. thanks everyone! getting up to speed fast
Mario Carneiro (Mar 22 2024 at 20:55):
or in the lakefile
Last updated: May 02 2025 at 03:31 UTC