Help understanding GADTs

Stream: lean4

[Juan Pablo Romero]

I'm having an issue understanding how type information flows in GADTs:

Expr has two parameters: a value A and an environment E.

inductive Expr : Type -> Type -> Type 1 where
  | done (a: A) : Expr Unit A
  | more (E A) (expr: Expr E A) : Expr E A

class Subset (E Provided: Type)


def eval (current: Expr E A) [inst: Subset E Provided] (env: Provided) : Unit :=
  match current with
  | .done a =>
    -- `E` should be equals to `Unit` here, no?
    ()

  | .more E1 _ expr =>
    -- `E` should be equals to `E1` here, no?

    /- ERROR: failed to synthesize instance Subset E1 Provided -/
    eval expr env

My assumption is that after pattern matching, on each branch the compiler has more information about specific types, for example in the .done case I expect that E is equal to Unit.

In the .more case, I expect that E is equal to E1. Clearly that's not the case, and so the implicit instance is not being picked up from the scope.

Any help would be appreciated.

[Henrik Böving]

First things first a little terminology: we don't really use the term GADT in Lean, this is an inductive type, more specifically a family of types indexed by the two other Type parameters.

Regarding your questions for equality in the branches, yes this is indeed the case and in fact you can make Lean tell you that this is the case by doing:

def eval (current: Expr E A) [inst: Subset E Provided] (env: Provided) : Unit :=
  match h:current with
  | .done a =>
    -- `E` should be equals to `Unit` here, no?
    ()

  | .more E1 _ expr =>
    -- `E` should be equals to `E1` here, no?

    /- ERROR: failed to synthesize instance Subset E1 Provided -/
    eval expr env

notice the h: at the match, in the done case this will give you:

: E = Unit
h : HEq current (Expr.done a)

and in the more one:

: E = E1
h : HEq current (Expr.more E1 A expr)

however usually you do not need these theorems in scope since the Lean dependent pattern matcher is smart enough to apply these facts to your local context. For example had your function had another argument of type E, namely foo:

def eval (foo : E) (current: Expr E A) [inst: Subset E Provided] (env: Provided) : Unit :=
  match current with
  | .done a =>
    ()
  | .more E1 _ expr =>
    sorry

you will in both branches observe that the dependent pattern matcher has intelligently changed the type of foo to Unit and E1 respectively.

Now in order to fix the error you have two choices here, one would be to use the h: approach to get the equivalence proof in the branch and then apply it with a ▸, the other would be to add the inst parameter to your pattern matcher because that will make it apply this theorem automatically again:

def eval (current: Expr E A) [inst: Subset E Provided] (env: Provided) : Unit :=
  match current, inst with
  | .done a, _ =>    ()
  | .more E1 _ expr, _ => eval expr env

I would personally prefer this one because it creates less burden on the user to figure out which theorem to apply where etc. but it does of course look a little magical as well since we are ignoring the result in both cases pretty much.

[Juan Pablo Romero]

Thanks!

[Notification Bot]

Juan Pablo Romero has marked this topic as resolved.

[Notification Bot]

Juan Pablo Romero has marked this topic as unresolved.

[Juan Pablo Romero]

Quick followup question: Is this a good way to get hold of inaccessible values?

let eq: E = E1 := by assumption

Or is there a way to avoid getting into tactic mode?

[pcpthm]

‹E = E1› (typed by \f< and \f>in vscode-lean) is a shorthand for show E = E1 by assumption.