Error with idiom brackets in equality type

Lambda.idr

module Lambda

%default total

infixr 8 ==>

data T : Type where
  U : T
  NAT : T
  (*) : T -> T -> T
  (+) : T -> T -> T
  (==>) : T -> T -> T

el : T -> Type
el U = ()
el NAT = Nat
el (t1 * t2) = (el t1, el t2)
el (t1 + t2) = Either (el t1) (el t2)
el (t1 ==> t2) = el t1 -> el t2

Context : (n : Nat) -> Type
Context n = Vect n T

data Term : (n : Nat) -> Context n -> T -> Type where
  Var : (i : Fin n) -> Term n g (index i g)
  Lam : Term (S n) (t :: g) t' -> Term n g (t ==> t')
  App : (Term n g (t1 ==> t2)) -> Term n g t1 -> Term n g t2

  Unit : Term n g U
  Zero : Term n g NAT
  Succ : Term n g NAT -> Term n g NAT
  NatRec : Term n g NAT -> Term n g t -> (Term n g (NAT ==> t ==> t)) -> Term n g t

{-
  Pair : Term n g t1 -> Term n g t2 -> Term n g (t1 * t2)
  Fst : Term n g (t1 * t2) -> Term n g t1
  Snd : Term n g (t1 * t2) -> Term n g t2
  Inl  : Term n g t1 -> Term n g (t1 + t2)
  Inr  : Term n g t2 -> Term n g (t1 + t2)
  Case : Term n g (t1 + t2) -> Term n g (t1 ==> tr) -> Term n g (t2 ==> tr) -> Term n g tr
-}


data Stack : Context n -> Type where
  Nil : Stack []
  (::) : {n : Nat} -> {g : Context n} ->
         (el t) -> Stack g -> Stack (t::g)

val : {n : Nat} -> {g : Context n} ->
      (i : Fin n) -> Stack g -> el (index i g)
val fZ     (v :: vs) = v
val (fS i) (v :: vs) = val i vs

interp : Term n g t -> Stack g -> el t
interp (Var i) s = val i s
interp {t=t1==>t2} (Lam b) s = \x : el t1 => interp b (x :: s)
interp (App e1 e2) s = (interp e1 s) (interp e2 s)
interp Unit s = ()
interp Zero _ = Z
interp (Succ n) s = S (interp n s)
interp (NatRec n base step) s = natrec (interp n s) (interp base s) (interp step s)
  where natrec : Nat -> a -> (Nat -> a -> a) -> a
        natrec Z      base _    = base
        natrec (S n') base step = step n' (natrec n' base step)

{-
interp (Pair e1 e2) s = (interp e1 s, interp e2 s)
interp (Fst e) s = fst (interp e s)
interp (Snd e) s = snd (interp e s)
interp (Inl e) s = Left (interp e s)
interp (Inr e) s = Right (interp e s)
interp (Case e l r) s =
  case interp e s of
    Left x => interp l s x
    Right y => interp r s y
-}

idNat : Term 0 [] (NAT ==> NAT)
idNat = Lam (Var 0)

plus : Term 0 [] (NAT ==> NAT ==> NAT)
plus = Lam (Lam (NatRec (Var 1) (Var 0) (Lam (Lam (Succ (Var 0))))))

five : Term 0 [] NAT
five = App (App plus (Succ (Succ Zero))) (Succ (Succ (Succ Zero)))


---------------------

dsl stlc
    lambda = Lam
    variable = Var
    index_first = fZ
    index_next = fS

-- nice!
idNat' : Term 0 [] (NAT ==> NAT)
idNat' = stlc (\x => x)

-- nice!
plus' : Term 0 [] (NAT ==> NAT ==> NAT)
plus' = stlc (\n, m => NatRec n m (\x, y => Succ y))

-- still ugly...
five' : Term 0 [] NAT
five' = App (App plus' (Succ (Succ Zero))) (Succ (Succ (Succ Zero)))


-- NB: this is <*>, not fmap
(<$>) : Term n g (t1 ==> t2) -> Term n g t1 -> Term n g t2
(<$>) e1 e2 = App e1 e2

pure : Term n g t -> Term n g t
pure x = x

-- much better!
five'' : Term 0 [] NAT
five'' = [| plus' (Succ (Succ Zero)) (Succ (Succ (Succ Zero))) |]


-- Nat syntax
%assert_total
fromInteger : Integer -> Term n g NAT
fromInteger n = if n > 0 then Succ (fromInteger (n - 1)) else Zero

five''' : Term 0 [] NAT
five''' = [| plus' 2 3 |]



------------------
-- Provisional definitions and tactic proofs
-----------------


fromNat : Nat -> Term n g NAT
fromNat Z = Zero
fromNat (S n) = Succ (fromNat n)

plusComm : (n, m : Nat) -> (interp [| plus' (fromNat n) (fromNat m) |] []) = (interp [| plus' (fromNat m) (fromNat n) |] [])
plusComm Z m = ?p
plusComm (S n) m = ?q

The error

*Lambda> :r
Type checking ./Lambda.idr
Lambda.idr:140:INTERNAL ERROR: "Something's gone wrong. Did you miss a semi-colon somewhere?"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
*Lambda>