max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 16:58:12 -07:00
parent fa3c32d3b1
commit de0eb8035f
1 changed files with 0 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
tests/lean/run/newfrontend4.lean
View file

@ -1,44 +0,0 @@
new_frontend
-- set_option syntaxMaxDepth 100
-- set_option trace.Elab true
-- set_option trace.Meta true
-- set_option trace.Meta.synthInstance false
def adapt1 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
⟨fun split join => monadMap @(fun α => adaptState split join : forall (α : Type), m α → m' α)⟩ -- monadMap (adaptState split join : m α → m' α)⟩
def adapt2 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
⟨fun split join => monadMap @(fun α => (adaptState split join : m α → m' α))⟩ -- monadMap (adaptState split join : m α → m' α)⟩
def adapt3 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
⟨fun split join => monadMap (m:=m) (m':=m') (adaptState split join)⟩
/-
The following fails because we cannot synthesize the instance
```
[MonadFunctorT
(λ (β : Type), m (?m_1 σ'' α split join β))
(λ (β : Type), m' (?m_1 σ'' α split join β))
n
(λ {α : Type}, n' α)]
```
Note that we have an instance `[MonadFunctorT m m' n n']`. The TC procedure performs eta-reduction, and manage to reduce
`(λ {α : Type}, n' α)` to `n'`, but it cannot eta-reduce the arguments
```
(λ (β : Type), m (?m_1 σ'' α split join β))
(λ (β : Type), m' (?m_1 σ'' α split join β))
```
The reduction is blocked by the metavariable applications `(?m_1 σ'' α split join β)`.
Remark: eta-expansion would also not solve the problem. The TC procedure would convert the instance
`[MonadFunctorT m m' n n']`
into
`[MonadFunctorT (fun β => m β) (fun β => m' β) (fun α => n α) (fun α => n' α)]`
but it would fail trying to unify
```
?m_1 σ'' α split join β =?= β
```
since `?m_1` was not created by the TC procedure. It was created by the elaborator.
-/
-- def adapt4 {m m' σ σ'} {n n' : Type → Type} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
-- ⟨fun split join => monadMap (adaptState split join : m _ → m' _)⟩ -- monadMap (adaptState split join : m α → m' α)⟩