Repository : ssh://[email protected]/ghc On branch : type-nats Link : http://ghc.haskell.org/trac/ghc/changeset/55113db0f75ad51c305b7cde19a2941ba0a78fb6/ghc
>--------------------------------------------------------------- commit 55113db0f75ad51c305b7cde19a2941ba0a78fb6 Author: Simon Peyton Jones <[email protected]> Date: Thu Aug 29 16:11:58 2013 +0100 Comments and questions from Simon and Dimitrios >--------------------------------------------------------------- 55113db0f75ad51c305b7cde19a2941ba0a78fb6 compiler/typecheck/TcTypeNats.hs | 13 ++++++++----- compiler/types/Coercion.lhs | 15 +++++++++++---- compiler/types/Type.lhs | 4 +++- compiler/types/TypeRep.lhs | 18 ++++++++++-------- 4 files changed, 32 insertions(+), 18 deletions(-) diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 4e1ce9f..639bdc4 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 @@ -174,8 +174,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. -} @@ -214,16 +214,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/Coercion.lhs b/compiler/types/Coercion.lhs index 734a99d..ed17596 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -139,16 +139,23 @@ data Coercion -- See Note [Forall coercions] | ForAllCo TyVar Coercion -- forall a. g - -- These are special | CoVarCo CoVar - | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely* - -- saturate arity of CoAxiom. - -- See [Coercion axioms applied to coercions] | UnsafeCo Type Type | SymCo Coercion | TransCo Coercion Coercion + -- Axioms + | AxiomInstCo CoAxiom [Coercion] -- The coercion arguments always *precisely* + -- saturate arity of CoAxiom. + -- See [Coercion axioms applied to coercions] + | TypeNatCo CoAxiomRule [Type] [Coercion] + -- An AxiomInstCo is like a degenerate TypeNatCo with empty [Coercion] + -- but in AxiomInstCo you can instantiate with [Coercion] not + -- only a [Type]. + + -- SPJ/DV: does the [Type] [Coercion] exactly saturate the + -- CoAxiomRule. Guess: yes; like AxiomInstCo. -- These are destructors | NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn) diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index bf5167a..482cb20 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -1675,12 +1675,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." diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index 70829fa..ee2163c 100644 --- a/compiler/types/TypeRep.lhs +++ b/compiler/types/TypeRep.lhs @@ -161,22 +161,24 @@ type SuperKind = Type \end{code} -% Rules for building Evidence -% --------------------------- - - -Conditional axioms. The genral idea is that a `CoAxiomRule` looks like this: +Note [CoAxiomRules] +~~~~~~~~~~~~~~~~~~~ +A CoAxiomRule is a conditional axiom. +The genral idea is that a `CoAxiomRule` looks like this: forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2 -My intension is to reuse these for both (~) and (~#). +My intention is to reuse these for both (~) and (~#). The short-term plan is to use this datatype to represent the type-nat axioms. In the longer run, it would probably be good to unify this and `CoAxiom`, as `CoAxiom` is the special case when there are no assumptions. -`CoAxiomTyLit` is used for axiom schemes defining equations between +`CoAxiomTyLit` is used for axiom *schemes* defining equations between type-literal constants. Currently, they contain no type variables -or assumptions. +or assumptions. Eg if + axr = CoAxiomTyList "add" (\n m -> Add n m ~ n+m) +and + TypeNatCo axr 3 4 :: Add 3 4 ~ 7 Note that if we think of equality as a (special) class: _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
