74bfa88 · Idris-dev · git.iko.soy

src/Idris/Elab/Term.hs+4−3

compare with master

unifiedsplit

@@ -16,7 +16,7 @@ import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

18import Idris.Core.ProofTerm (getProofTerm)

19−import Idris.Core.Typecheck (check, recheck, isType)

19+import Idris.Core.Typecheck (check, recheck, converts, isType)

20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21import Idris.ErrReverse (errReverse)

22import Idris.ElabQuasiquote (extractUnquotes)

@@ -1720,8 +1720,9 @@ runTactical ist fc env tm = do tm' <- eval tm

1720 let info = CaseInfo True True False -- TODO document and figure out

1721 clauses' <- forM clauses (\case

1722 RMkFunClause lhs rhs ->

1723− do lhs' <- fmap fst . lift $ check ctxt [] lhs

1723+ do (lhs', lty) <- lift $ check ctxt [] lhs

1724− rhs' <- fmap fst . lift $ check ctxt [] rhs

1724+ (rhs', rty) <- lift $ check ctxt [] rhs

1725+ lift $ converts ctxt [] lty rty

1725 return $ Right (lhs', rhs')

1726 return $ Right (lhs', rhs')

1726 RMkImpossibleClause lhs ->

1727 RMkImpossibleClause lhs ->

1727 do lhs' <- fmap fst . lift $ check ctxt [] lhs

1728 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