@@ -1782,6 +1782,25 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17821782 pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
17831783 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
17841784
1785+ requireError :: Err -> ElabD a -> ElabD ()
1786+ requireError orErr elab =
1787+ do state <- get
1788+ case runStateT elab state of
1789+ OK (_, state') -> lift (tfail orErr)
1790+ Error e -> return ()
1791+
1792+ -- create a fake TT term for the LHS of an impossible case
1793+ fakeTT :: Raw -> Term
1794+ fakeTT (Var n) =
1795+ case lookupNameDef n (tt_ctxt ist) of
1796+ [(n', TyDecl nt _)] -> P nt n' Erased
1797+ _ -> P Ref n Erased
1798+ fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)
1799+ fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)
1800+ fakeTT RType = TType (UVar (-1))
1801+ fakeTT (RUType u) = UType u
1802+ fakeTT (RConstant c) = Constant c
1803+
17851804 defineFunction :: RFunDefn Raw -> ElabD ()
17861805 defineFunction (RDefineFun n clauses) =
17871806 do ctxt <- get_context
@@ -1794,10 +1813,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
17941813 lift $ converts ctxt [] lty rty
17951814 return $ Right (lhs', rhs')
17961815 RMkImpossibleClause lhs ->
1797− do lhs' <- fmap fst . lift $ check ctxt [] lhs
1798− return $ Left lhs')
1816+ do requireError (Msg "Not an impossible case") . lift $
1817+ check ctxt [] lhs
1818+ return $ Left (fakeTT lhs))
17991819 let clauses'' = map (\case Right c -> pullVars c
1800− Left lhs -> let (ns, lhs') = patvars [] lhs'
1820+ Left lhs -> let (ns, lhs') = patvars [] lhs
18011821 in (ns, lhs', Impossible))
18021822 clauses'
18031823 let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''