Type check definitions added during Elab reflection

src/Idris/Elab/Term.hs

@@ -16,7 +16,7 @@ import Idris.Core.TT
 import Idris.Core.Evaluate
 import Idris.Core.Unify
 import Idris.Core.ProofTerm (getProofTerm)
-import Idris.Core.Typecheck (check, recheck, isType)
+import Idris.Core.Typecheck (check, recheck, converts, isType)
 import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
 import Idris.ErrReverse (errReverse)
 import Idris.ElabQuasiquote (extractUnquotes)
@@ -1720,8 +1720,9 @@ runTactical ist fc env tm = do tm' <- eval tm
          let info = CaseInfo True True False -- TODO document and figure out
          clauses' <- forM clauses (\case
                                       RMkFunClause lhs rhs ->
-                                        do lhs' <- fmap fst . lift $ check ctxt [] lhs
-                                           rhs' <- fmap fst . lift $ check ctxt [] rhs
+                                        do (lhs', lty) <- lift $ check ctxt [] lhs
+                                           (rhs', rty) <- lift $ check ctxt [] rhs
+                                           lift $ converts ctxt [] lty rty
                                            return $ Right (lhs', rhs')
                                       RMkImpossibleClause lhs ->
                                         do lhs' <- fmap fst . lift $ check ctxt [] lhs

test/meta003/BadDef.idr

@@ -0,0 +1,12 @@
+module BadDef
+
+import Language.Reflection.Elab
+
+mkN : String -> TTName
+mkN n = NS (UN n) ["BadDef"]
+
+mkBadDef1 : Elab ()
+mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())
+               defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]
+runBad1 : ()
+runBad1 = %runElab (mkBadDef1 *> search)

test/meta003/expected

@@ -0,0 +1,6 @@
+BadDef.idr:12:9:
+When checking right hand side of runBad1:
+Type mismatch between
+        ()
+and
+        String

test/meta003/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ --nocolour --check --consolewidth 70 BadDef.idr
+rm -f *.ibc