fd9e0fb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce)

(And the crowd goes wild)

commitfd9e0fb23a49deec86da5b0a0286fcb9e6db5a0a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 28 Mar 2013, 12:16 (14 years ago) parente3a4097

4 files changed+12−3

compare with master

unifiedsplit

src/Core/ProofState.hs+2−2 src/Core/TT.hs+2 src/Core/Typecheck.hs+1−1 src/Idris/Delaborate.hs+7

src/Core/ProofState.hs+2−2

@@ -422,7 +422,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

422422 let (uh, uns) = unified ps

423423-- put (ps { unified = (uh, uns ++ ns) })

424424 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

425− _ -> fail "Nothing to introduce"

425+ _ -> lift $ tfail $ CantIntroduce t'

426426introTy ty n ctxt env _ = fail "Can't introduce here."

427427

428428intro :: Maybe Name -> RunTactic

@@ -437,7 +437,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

437437 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

438438 let t' = instantiate (P Bound n s) (pToV y t) in

439439 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

440− _ -> fail "Nothing to introduce"

440+ _ -> lift $ tfail $ CantIntroduce t'

441441intro n ctxt env _ = fail "Can't introduce here."

442442

443443forall :: Name -> Raw -> RunTactic

src/Core/TT.hs+2

@@ -57,6 +57,8 @@ data Err = Msg String

5757 -- unification succeed

5858 | InfiniteUnify Name Term [(Name, Type)]

5959 | CantConvert Term Term [(Name, Type)]

60+ | NonFunctionType Term Term

61+ | CantIntroduce Term

6062 | NoSuchVariable Name

6163 | NoTypeDecl Name

6264 | NotInjective Term Term Term

src/Core/Typecheck.hs+1−1

@@ -81,7 +81,7 @@ check' holes ctxt env top = chk env top where

8181 let apty = simplify initContext False env

8282 (Bind x (Let aty av) t)

8383 return (App fv av, apty)

84− t -> fail "Can't apply a non-function type"

84+ t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"

8585 -- This rather unpleasant hack is needed because during incomplete

8686 -- proofs, variables are locally bound with an explicit name. If we just

8787 -- make sure bound names in function types are locally unique, machine

src/Idris/Delaborate.hs+7

@@ -90,6 +90,13 @@ pshow i (CantConvert x y env)

9090 "Can't convert " ++ showImp imps (delab i x) ++ " with "

9191 ++ showImp imps (delab i y) ++

9292 if (opt_errContext (idris_options i)) then showSc i env else ""

93+pshow i (NonFunctionType f ty)

94+ = let imps = opt_showimp (idris_options i) in

95+ showImp imps (delab i f) ++ " does not have a function type ("

96+ ++ showImp imps (delab i ty) ++ ")"

97+pshow i (CantIntroduce ty)

98+ = let imps = opt_showimp (idris_options i) in

99+ "Can't use lambda here: type is " ++ showImp imps (delab i ty)

93100pshow i (InfiniteUnify x tm env)

94101 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

95102 " would lead to infinite value" ++