git.iko.soy/Idris-dev
on master help sign in
Fix the new totality test
ef954e1David Raymond Christiansen
src/Idris/AbsSyntax.hs+5−1
compare with master
unifiedsplit
@@ -1734,7 +1734,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
1734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
1735 = Placeholder
1735 = Placeholder
1736 su (PApp fc f@(PRef _ fn) args)
1736 su (PApp fc f@(PRef _ fn) args)
1737− | isDConName fn ctxt
1737+ -- here we use canBeDConName because the impossible pattern
1738+ -- check will not necessarily fully resolve constructor names,
1739+ -- and these bare names will otherwise get in the way of
1740+ -- impossbility checking.
1741+ | canBeDConName fn ctxt
1738 = PApp fc f (fmap (fmap su) args)
1742 = PApp fc f (fmap (fmap su) args)
1739 su (PApp fc f args)
1743 su (PApp fc f args)
1740 = PHidden (PApp fc f args)
1744 = PHidden (PApp fc f args)
src/Idris/Core/Evaluate.hs+10−1
@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 mapDefCtxt,
13 mapDefCtxt,
14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,
14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
16 isUniverse) where
16 isUniverse) where
17
17
@@ -975,12 +975,21 @@ isTConName n ctxt
975 Just (TyDecl (TCon _ _) _) -> True
975 Just (TyDecl (TCon _ _) _) -> True
976 _ -> False
976 _ -> False
977
977
978+-- | Check whether a resolved name is certainly a data constructor
978isDConName :: Name -> Context -> Bool
979isDConName :: Name -> Context -> Bool
979isDConName n ctxt
980isDConName n ctxt
980 = case lookupDefExact n ctxt of
981 = case lookupDefExact n ctxt of
981 Just (TyDecl (DCon _ _ _) _) -> True
982 Just (TyDecl (DCon _ _ _) _) -> True
982 _ -> False
983 _ -> False
983
984
985+-- | Check whether any overloading of a name is a data constructor
986+canBeDConName :: Name -> Context -> Bool
987+canBeDConName n ctxt
988+ = or $ do def <- lookupCtxt n (definitions ctxt)
989+ case tfst def of
990+ (TyDecl (DCon _ _ _) _) -> return True
991+ _ -> return False
992+
984isFnName :: Name -> Context -> Bool
993isFnName :: Name -> Context -> Bool
985isFnName n ctxt
994isFnName n ctxt
986 = case lookupDefExact n ctxt of
995 = case lookupDefExact n ctxt of
src/Idris/Delaborate.hs+1−1
@@ -308,7 +308,7 @@ pprintErr' i (ElaboratingArg f x _ e)
308 where whatIsName = let ctxt = tt_ctxt i
308 where whatIsName = let ctxt = tt_ctxt i
309 in if isTConName f ctxt
309 in if isTConName f ctxt
310 then text "type constructor" <> space
310 then text "type constructor" <> space
311− else if isConName f ctxt
311+ else if isDConName f ctxt
312 then text "constructor" <> space
312 then text "constructor" <> space
313 else if isFnName f ctxt
313 else if isFnName f ctxt
314 then text "function" <> space
314 then text "function" <> space