[commit: ghc] type-nats: Comments and questions from Simon and Dimitrios (55113db)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : type-nats
Link       : http://ghc.haskell.org/trac/ghc/changeset/55113db0f75ad51c305b7cde19a2941ba0a78fb6/ghc

>---------------------------------------------------------------

commit 55113db0f75ad51c305b7cde19a2941ba0a78fb6
Author: Simon Peyton Jones <simonpj at microsoft.com>
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: