fd9e0fb · Idris-dev · git.iko.soy

src/Core/ProofState.hs+2−2

compare with master

unifiedsplit

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

422 let (uh, uns) = unified ps

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

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

425− _ -> fail "Nothing to introduce"

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

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

427

428intro :: Maybe Name -> RunTactic

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

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

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

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

440− _ -> fail "Nothing to introduce"

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

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

442

443forall :: Name -> Raw -> RunTactic

src/Core/TT.hs+2

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

57 -- unification succeed

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

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

60+ | NonFunctionType Term Term

61+ | CantIntroduce Term

60 | NoSuchVariable Name

62 | NoSuchVariable Name

61 | NoTypeDecl Name

63 | NoTypeDecl Name

62 | NotInjective Term Term Term

64 | NotInjective Term Term Term

src/Core/Typecheck.hs+1−1

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

81 let apty = simplify initContext False env

82 (Bind x (Let aty av) t)

83 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"

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

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

87 -- 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)

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

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

92 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)

93pshow i (InfiniteUnify x tm env)

100pshow i (InfiniteUnify x tm env)

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

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

95 " would lead to infinite value" ++

102 " would lead to infinite value" ++