git.iko.soy/Idris-dev
on master help sign in
Type check definitions added during Elab reflection
commit74bfa88683c4781db462f92861dad3ffd653d359 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 4 Jun 2015, 11:09 (11 years ago) parentbf6dbf9
4 files changed+25−3
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+4−3 test/meta003/BadDef.idr+12 test/meta003/expected+6 test/meta003/run+3
src/Idris/Elab/Term.hs+4−3
@@ -16,7 +16,7 @@ import Idris.Core.TT
1616import Idris.Core.Evaluate
1717import Idris.Core.Unify
1818import Idris.Core.ProofTerm (getProofTerm)
19−import Idris.Core.Typecheck (check, recheck, isType)
19+import Idris.Core.Typecheck (check, recheck, converts, isType)
2020import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
2121import Idris.ErrReverse (errReverse)
2222import Idris.ElabQuasiquote (extractUnquotes)
@@ -1720,8 +1720,9 @@ runTactical ist fc env tm = do tm' <- eval tm
17201720 let info = CaseInfo True True False -- TODO document and figure out
17211721 clauses' <- forM clauses (\case
17221722 RMkFunClause lhs rhs ->
1723− do lhs' <- fmap fst . lift $ check ctxt [] lhs
1724− rhs' <- fmap fst . lift $ check ctxt [] rhs
1723+ do (lhs', lty) <- lift $ check ctxt [] lhs
1724+ (rhs', rty) <- lift $ check ctxt [] rhs
1725+ lift $ converts ctxt [] lty rty
17251726 return $ Right (lhs', rhs')
17261727 RMkImpossibleClause lhs ->
17271728 do lhs' <- fmap fst . lift $ check ctxt [] lhs
test/meta003/BadDef.idrnew file+12
@@ -0,0 +1,12 @@
1+module BadDef
2+
3+import Language.Reflection.Elab
4+
5+mkN : String -> TTName
6+mkN n = NS (UN n) ["BadDef"]
7+
8+mkBadDef1 : Elab ()
9+mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())
10+ defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]
11+runBad1 : ()
12+runBad1 = %runElab (mkBadDef1 *> search)
test/meta003/expectednew file+6
@@ -0,0 +1,6 @@
1+BadDef.idr:12:9:
2+When checking right hand side of runBad1:
3+Type mismatch between
4+ ()
5+and
6+ String
test/meta003/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --nocolour --check --consolewidth 70 BadDef.idr
3+rm -f *.ibc