Pattern matching and some constructors simply does not works

Stream: new members

[Felipe GS]

inductive Lemon : Type 0 → Type 1 where
  | pure    : t → Lemon t
  | seq     : Lemon (u → t) → Lemon u → Lemon t
  | satisfy : (Char → Bool) → Lemon String

-- tactic 'cases' failed, nested error:
-- dependent elimination failed, failed to solve equation
--  Int = String
-- at case Lemon.satisfy after processing

def test : Lemon Int → Int
  | Lemon.pure x => 2
  | Lemon.seq x y => 2

Why can't I do that? I tried with casesOn but for some reason the first functions does not unifies with Int so I simply cant remove the value from inside of the pure!

If the result type in the data constructor is different from a type variable, it always fail in a pattern match :\

[Reid Barton]

Int could be equal to String so Lean cannot eliminate the possibility of Lemon.satisfy.

[Reid Barton]

If you are coming from Haskell, then this will look strange

[Felipe GS]

So.. how should I rewrite this code to make something like that work? I think that Lemon.satisfy is useful so I cannot simply remove this constructor :\

[Kevin Buzzard]

Why not just return 37 in the satisfy case?

[Reid Barton]

I guess in a real interpreter you will have to handle all possible type indices anyways (for seq), like Lemon a -> a, so this issue won't come up

[Felipe GS]

Yeah but I'm trying to make a function to optimize the ast so seq (pure f) (pure x) becomes pure (f x) but I cannot pattern match on the first constructor because the type is Lemon (u -> t) (When I add another constructor | empty : Lemon Unit)

[Felipe GS]

Kevin Buzzard said:

Why not just return 37 in the satisfy case?

  /--
  type mismatch
    Lemon.satisfy x
  has type
    Lemon String : Type 1
  but is expected to have type
    Lemon Int : Type 1
  -/
  def test : Lemon Int → Int
    | Lemon.seq f x => 1
    | Lemon.pure x => 2
    | Lemon.satisfy x => 3

[Reid Barton]

Not sure how smart the equation compiler is on this sort of thing. This works at least:

  def test' : Lemon a → a = Int → Int
    | Lemon.seq f x, _ => 1
    | Lemon.pure x, _ => 2
    | Lemon.satisfy x, _ => 3

  def test : Lemon Int → Int
    | x => test' x rfl

[Reid Barton]

I would need a real example to give a real suggestion.

[Reid Barton]

A silly suggestion: If you really wanted to, you could add an axiom saying Int and String are distinct (which is certainly consistent) and then use False.elim in the "impossible" case.

[Felipe GS]

How should I fix that?

inductive Lemon : Type 0 → Type 1 where
  | pure    : t → Lemon t
  | seq     : Lemon (u → t) → Lemon u → Lemon t
  | satisfy : (Char → Bool) → Lemon String
  | empty   : Lemon Unit

/--
tactic 'cases' failed, nested error:
dependent elimination failed, failed to solve equation
  (u✝ → α) = String
at case Lemon.satisfy after processing
  (@Lemon.seq _ _ _ (@Lemon.pure _ _))
the dependent pattern matcher can solve the following kinds of equations
-/

def opt : Lemon α → Lemon α
  | Lemon.seq (Lemon.pure f) (Lemon.pure x) => Lemon.pure (f x)
  | r => r

[Reid Barton]

I think the equation compiler just doesn't know how to handle this situation (yet?). Here is one way to do it:

inductive Lemon (a b : Type) : Type 0 → Type 1 where
  | pure    : t → Lemon a b t
  | seq     : Lemon a b (u → t) → Lemon a b u → Lemon a b t
  | satisfy : (Char → Bool) → Lemon a b a
  | empty   : Lemon a b b

def opt : Lemon a b α → Lemon a b α
  | Lemon.seq (Lemon.pure f) (Lemon.pure x) => Lemon.pure (f x)
  | r => r

[Reid Barton]

If you need to know a = String in some other case, you can pass in an equality hypothesis like in test'