6625656940
The semantics was weird. It seems Agda is also having problems with
it. Here is an example that demonstrates how weird the semantics is:
```lean
check (fun {β α} (a : α) (b : β) => (b, a) : {α : Type} → {β : Type} → (a : α) → (b : β) → β × α)
-- Same example using `def`
def f : {α : Type} → {β : Type} → α → β → β × α :=
fun {β : Type} {α : Type} (a : α) (b : β) => (b, a)
```
Both commands were being accepted before this commit. Note that it
flips `β` and `α`.
Here is an example that did not work before this commit and would
confuse users.
```lean
check
let id := fun {α} (a : α) => a;
id [id 1]
```
users would have to write
```lean
check
let id {α} (a : α) := a;
id [id 1]
```
@Kha The Delaborator.lean test broke and I "fixed" by removing the
`{}` from it, and copying `produced` over `expected`. Please make sure
it still makes sense.
65 lines
1.9 KiB
Text
65 lines
1.9 KiB
Text
def foo {α} (f : forall {β}, β → β) (a : α) : α :=
|
||
f a
|
||
|
||
new_frontend
|
||
|
||
#check_failure let g := id; foo g true -- fails
|
||
/-
|
||
Expands to
|
||
```
|
||
let g : ?γ → ?γ := @id ?γ;
|
||
@foo ?α (fun (β : Sort ?u) => g) true
|
||
```
|
||
|
||
Unification constraint
|
||
```
|
||
?γ → ?γ =?= β → β
|
||
```
|
||
fails because `β` is not in the scope of `?γ`
|
||
|
||
Error message can be improved because it doesn't make it clear
|
||
the issue is the scope of the metavariable. Not sure yet how to improve it.
|
||
-/
|
||
#check_failure (fun g => foo g 2) id -- fails for the same reason the previous one fail.
|
||
|
||
#check let g := @id; foo @g true -- works
|
||
/-
|
||
Expands into
|
||
```
|
||
let g : {γ : Sort ?v} → γ → γ := @id;
|
||
@foo ?α @g true
|
||
```
|
||
Note that `@g` also disables implicit lambdas.
|
||
The unification constraint is easily solved
|
||
```
|
||
{γ : Sort ?v} → γ → γ =?= {β : Sort ?u} → β → β
|
||
```
|
||
-/
|
||
|
||
#check foo id true -- works
|
||
#check foo @id true -- works
|
||
#check foo (fun b => b) true -- works
|
||
#check foo @(fun β b => b) true -- works
|
||
#check_failure foo @(fun b => b) true -- fails as expected, and error message is clear
|
||
#check foo @(fun β b => b) true -- works (implicit lambdas were disabled)
|
||
|
||
|
||
set_option pp.all true
|
||
|
||
#check let x := (fun f => (f, f)) @id; (x.1 (), x.2 true) -- works
|
||
#check_failure let x := (fun f => (f, f)) id; (x.1 (), x.2 true) -- fails as expected
|
||
-- #check let x := (fun (f : {α : Type} → α → α) => (f, f)) @id; (x.1 (), x.2 true) -- we need constApprox := true for this one
|
||
-- #check let x := (fun (f : {α : Type} → α → α) => (f, f)) @id; (x.1 [], x.2 true) -- we need constApprox := true for this one
|
||
|
||
set_option pp.all false
|
||
set_option pp.implicit true
|
||
|
||
def h (x := 10) (y := 20) : Nat := x + y
|
||
#check h -- h 10 20 : Nat
|
||
#check let f := @h; f -- (let f : optParam Nat 10 → optParam Nat 20 → Nat := @h; f 10 20) : Nat
|
||
|
||
#check_failure let f := fun (x : optParam Nat 10) => x + 1; f + f 1
|
||
#check_failure (fun (x : optParam Nat 10) => x)
|
||
|
||
|
||
#check let! x := 10; x + 1
|