Compiling flat vector doesn't terminate

[eayus]

Not sure whether this is known behaviour, but compileing the following example doesn't terminate (it checks fine)

data Nat where
  Zero : Nat
  Succ : Nat -> Nat

Pair : Type -> Type -> Type

data Pair a b where
  MkPair : a -> b -> Pair a b

data Unit where
  MkUnit : Unit

Vector : Nat -> Type -> Type
Vector Zero _ = Unit
Vector (Succ n) a = Pair a (Vector n a)

[ollef]

Hey, and thanks for reaching out! The backend is quite unfinished, so I'm not too surprised at this stage. Most of my effort has gone into the type checker so far, but I'm hoping to do more work on the backend eventually. :)