Type mismatch with pattern matching and lets

[gebner]

import Lean
open Lean Meta

def substIssue (hLocalDecl : LocalDecl) : MetaM Unit := do
  let error {α} _ : MetaM α := throwError "{hLocalDecl.type}"
  let some (_, lhs, rhs) ← matchEq? hLocalDecl.type | error ()
  error ()

prints:

extracted.lean:4:4: error: type mismatch at `_x.77`, value has type
  EStateM.Result Exception PUnit _y.240
but is expected to have type
  EStateM.Result Exception PUnit α

Nightly: leanprover/lean4:nightly-2022-10-04

[leodemoura]

@hargoniX The type error occurs after the extendJoinPointContext. Some observations

• findJoinPoints converts the local function error into a join point. This creates a special situation because we now have a join point that takes a type parameter α as an argument.
• The function LocalDecl.type is inlined and a nested join point. The nested join point depends on α
• extendJoinPointContext abstracts α in this nested join point producing type incorrect code.

One solution is to track whether the parameter occurs in a type and don't abstract it. Another option is to invoke the transformation only on phase 2 after we have erased type parameters.

cc @digama0

[leodemoura]

I will disable the extendJoinPointContext pass for now to make sure @gebner can bump mathlib.

[leodemoura]

@hargoniX I didn't look at the bug in detail, but I think we can fix this issue by applying the substitution from free-variables to parameters to all types. For example, the type of the nested join point should be

MessageData →
Core.Context →
ST.Ref PUnit Core.State →
Type → Context → PUnit → ST.Ref PUnit State → Expr → EStateM.Result Exception PUnit _y.240 --- << instead of alpha

[hargoniX]

Taking a look!