diff options
| -rw-r--r-- | compiler/typecheck/TcTypeNats.hs | 13 | ||||
| -rw-r--r-- | compiler/types/Type.lhs | 4 |
2 files changed, 11 insertions, 6 deletions
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 019b22e0de..abbf359979 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -1,4 +1,4 @@ -module TcTypeNats where +module TcTypeNats( typeNatStage ) where import PrelNames( typeNatAddTyFamName , typeNatMulTyFamName @@ -288,8 +288,8 @@ ppImp qs q = pprWithCommas p qs <+> text "=>" <+> p q -------------------------------------------------------------------------------- -{- See if the constraint is "obvious" (i.e., it can be solved by an -axiom with no preconditions). We apply this not only to wanteds, which may +{- See if the constraint is "obvious" (i.e., it can be solved by a +build-in axiom with no preconditions). We apply this not only to wanteds, which may simply get solved by it, but also to new given and derived constraints. Given and dervied constraints that can be solved in this way are ignored because they would not be contributing any new information. -} @@ -339,16 +339,19 @@ solveByIff ct impossible :: Ct -> Bool - +-- Some ad-hoc checks for un-satisfiable constraints impossible (CFunEqCan { cc_fun = tc, cc_tyargs = [t1,t2], cc_rhs = t3 }) | name == typeNatAddTyFamName = case (mbA,mbB,mbC) of + -- na + ? = nc requires na <= nc (Just a, _ , Just c) -> isNothing (minus c a) (_ , Just b, Just c) -> isNothing (minus c b) + + -- na + b = c, a > 0 requires b /= c (Just a, _ , _) | a > 0 -> eqType t2 t3 (_ , Just b, _) | b > 0 -> eqType t1 t3 - _ -> False + _ -> False | name == typeNatMulTyFamName = case (mbA,mbB,mbC) of diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 05651cc4a2..69317518f9 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -1691,12 +1691,14 @@ co_axr_tynum2_rule n f = co_axr_tylit_rule n toEqn toEqn _ = panic "`co_axr_tynum2_rule` requires 2 numeric literals." co_axr_inst :: CoAxiomRule -> [Type] -> ([Eqn], Eqn) +-- (co_axr_inst axr tys) instantiates 'axr' at types 'tys', +-- returning (eqn_1, .., eqn_n) => eqn co_axr_inst (CoAxiomRule _ vs as c) ts = (map inst2 as, inst2 c) where inst = substTyWith vs ts inst2 (a,b) = (inst a, inst b) co_axr_inst (CoAxiomTyLit _ f) ts = - case mapM isTyLit ts of + case mapM isTyLit ts of -- All type args must be TyLits Just tls -> ([], f tls) Nothing -> pprPanic "co_axr_inst" (vcat ( text "CoAxiomTyLit was used with a non-literal type." |