[commit: ghc] type-nats-simple: Generalize CoAxiomRule to support non-nominal Roles. Add coreLint checks. (cf2b52b)

[git at git.haskell.org]

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

On branch  : type-nats-simple
Link       : http://ghc.haskell.org/trac/ghc/changeset/cf2b52bb7ce82f47b146eabe78ddde8ae164dcf1/ghc

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

commit cf2b52bb7ce82f47b146eabe78ddde8ae164dcf1
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat Sep 7 13:43:30 2013 -0700

    Generalize CoAxiomRule to support non-nominal Roles.  Add coreLint checks.


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

cf2b52bb7ce82f47b146eabe78ddde8ae164dcf1
 compiler/coreSyn/CoreLint.lhs    |   42 ++++++++++++++++++++++++++++++--------
 compiler/typecheck/TcTypeNats.hs |    6 ++++--
 compiler/types/CoAxiom.lhs       |    5 +++--
 compiler/types/Coercion.lhs      |    2 +-
 compiler/types/OptCoercion.lhs   |    4 ++--
 5 files changed, 43 insertions(+), 16 deletions(-)

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 3d5e93a..57604b3 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -981,22 +981,46 @@ lintCoercion this@(AxiomRuleCo co ts cs)
   = do _ks <- mapM lintType ts
        eqs <- mapM lintCoercion cs
 
-       let unexpected_roles = [ r | (_,_,_,r) <- eqs, r /= Nominal ]
-       unless (null unexpected_roles) $
-          failWithL $ err "CoAxiomRule applied to non-nominal coercion(s)"
-                          (map ppr unexpected_roles)
+       let tyNum = length ts
+
+       case compare (coaxrTypeArity co) tyNum of
+         EQ -> return ()
+         LT -> err "Too many type arguments"
+                    [ txt "expected" <+> int (coaxrTypeArity co)
+                    , txt "provided" <+> int tyNum ]
+         GT -> err "Not enough type arguments"
+                    [ txt "expected" <+> int (coaxrTypeArity co)
+                          , txt "provided" <+> int tyNum ]
+       checkRoles 0 (coaxrAsmpRoles co) eqs
 
        case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
-         Nothing -> failWithL $ err "Malformed use of AxiomRuleCo" [ ppr this ]
+         Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
          Just (Pair l r) ->
            do kL <- lintType l
               kR <- lintType r
-              checkL (eqKind kL kR)
-                $ err "Kind error in CoAxiomRule" [ppr kL <+> txt "/=" <+> ppr kR]
-              return (kL, l, r, Nominal)
+              unless (eqKind kL kR)
+                $ err "Kind error in CoAxiomRule"
+                       [ppr kL <+> txt "/=" <+> ppr kR]
+              return (kL, l, r, coaxrRole co)
   where
   txt       = ptext . sLit
-  err m xs  = hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+  err m xs  = failWithL $
+                hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
+
+  checkRoles n (e : es) ((_,_,_,r) : rs)
+    | e == r    = checkRoles (n+1) es rs
+    | otherwise = err "Argument roles mismatch"
+                      [ txt "In argument:" <+> int (n+1)
+                      , txt "Expected:" <+> ppr e
+                      , txt "Found:" <+> ppr r ]
+  checkRoles _ [] []  = return ()
+  checkRoles n [] rs  = err "Too many coercion arguments"
+                          [ txt "Expected:" <+> int n
+                          , txt "Provided:" <+> int (n + length rs) ]
+
+  checkRoles n es []  = err "Not enough coercion arguments"
+                          [ txt "Expected:" <+> int (n + length es)
+                          , txt "Provided:" <+> int n ]
 
 \end{code}
 
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 289b0e8..87ed825 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -158,7 +158,8 @@ mkBinAxiom str tc f =
   CoAxiomRule
     { coaxrName      = fsLit str
     , coaxrTypeArity = 2
-    , coaxrAsmpArity = 0
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
     , coaxrProves    = \ts cs ->
         case (ts,cs) of
           ([s,t],[]) -> do x <- isNumLitTy s
@@ -173,7 +174,8 @@ mkAxiom1 str f =
   CoAxiomRule
     { coaxrName      = fsLit str
     , coaxrTypeArity = 1
-    , coaxrAsmpArity = 0
+    , coaxrAsmpRoles = []
+    , coaxrRole      = Nominal
     , coaxrProves    = \ts cs ->
         case (ts,cs) of
           ([s],[]) -> return (f s)
diff --git a/compiler/types/CoAxiom.lhs b/compiler/types/CoAxiom.lhs
index c750321..671e857 100644
--- a/compiler/types/CoAxiom.lhs
+++ b/compiler/types/CoAxiom.lhs
@@ -487,8 +487,9 @@ type Eqn = Pair Type
 -- | For now, we work only with nominal equality.
 data CoAxiomRule = CoAxiomRule
   { coaxrName      :: FastString
-  , coaxrTypeArity :: Int
-  , coaxrAsmpArity :: Int
+  , coaxrTypeArity :: Int       -- number of type argumentInts
+  , coaxrAsmpRoles :: [Role]    -- roles of parameter equations
+  , coaxrRole      :: Role      -- role of resulting equation
   , coaxrProves    :: [Type] -> [Eqn] -> Maybe Eqn
     -- ^ This returns @Nothing@ when we don't like
     -- the supplied arguments.
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 77d280e..49e37fa 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1784,7 +1784,7 @@ coercionRole = go
     go (LRCo _ _)           = Nominal
     go (InstCo co _)        = go co
     go (SubCo _)            = Representational
-    go (AxiomRuleCo _ _ _)  = Nominal
+    go (AxiomRuleCo c _ _)  = coaxrRole c
 \end{code}
 
 Note [Nested InstCos]
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index 3397ca7..1a06445 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -227,9 +227,9 @@ opt_co' env sym _ (SubCo co) = opt_co env sym (Just Representational) co
 -- XXX: We could add another field to CoAxiomRule that
 -- would allow us to do custom simplifications.
 opt_co' env sym mrole (AxiomRuleCo co ts cs) =
-  wrapRole mrole Nominal $
+  wrapRole mrole (coaxrRole co) $
     AxiomRuleCo co (map (substTy env) ts)
-                   (map (opt_co env sym (Just Nominal)) cs)
+                   (zipWith (opt_co env sym) (map Just (coaxrAsmpRoles co)) cs)