GADT trouble

Stream: general

[Alice Laroche]

I have this :

inductive regex : nat -> Type*
| emp         : regex 0
| chr         : char -> regex 0
| group       : nat -> regex n -> regex (n + 1)
| alt   (m n) : regex m -> regex n -> regex (m + n)
| conct (m n) : regex m -> regex n -> regex (m + n)
open regex

instance {n' : nat } : has_sizeof (regex n') :=
⟨
  λreg, match reg with
      | alt m n r r' := 0
      | _ := 0
      end
⟩

And i have this error :

type mismatch at application
  _match (alt m n r r')
term
  alt m n r r'
has type
  regex (m + n) : Type ?
but is expected to have type
  regex n' : Type ?

I understand why, but i don't know how to fix this

[Zhanrong Qiao]

You can match on both n' and reg:

instance {n' : nat} : has_sizeof (regex n') :=
  ⟨λ reg,
    match n', reg with
    | _, emp            := 0
    | _, chr c          := 0
    | _, group n r      := 0
    | _, alt m n r r'   := 0
    | _, conct m n r r' := 0
    end⟩

This is called "dependent pattern matching"

[Alice Laroche]

Thanks