  case infer env ctx t of
    Left err -> Left (TypeErr i err)
    Right v  -> Right (Map.insert x v env, ctx)
runRepl i (env, ctx) (DefineCheck x a t) =
  if x `Map.member` env then Left (EnvErr i x) else
  case check env ctx a (NfS (Type 0)) of
    Left err -> case check env ctx a (NfS (Type 1)) of
      Left err -> Left (TypeErr i err)
      Right a -> case check env ctx t a of
        Left err -> Left (TypeErr i err)