Repository : ssh://[email protected]/ghc On branch : type-nats-simple Link : http://ghc.haskell.org/trac/ghc/changeset/cf2b52bb7ce82f47b146eabe78ddde8ae164dcf1/ghc
>--------------------------------------------------------------- commit cf2b52bb7ce82f47b146eabe78ddde8ae164dcf1 Author: Iavor S. Diatchki <[email protected]> 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) _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
