More import tidying and fixing the stage 2 build

[ghc-hetmet.git] / compiler / types / Coercion.lhs

diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 25d04ec..672deae 100644 (file)
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1,5 +1,8 @@
+%
+% (c) The University of Glasgow 2006
+%

 
 

- Module for type coercions, as in System FC.
+Module for type coercions, as in System FC.

 
 Coercions are represented as types, and their kinds tell what types the 
 coercion works on. 
 
 Coercions are represented as types, and their kinds tell what types the 
 coercion works on. 

@@ -22,7 +25,7 @@ module Coercion (
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,

-        mkNewTypeCoercion, mkAppsCoercion,
+        mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion,

 
         splitNewTypeRepCo_maybe, decomposeCo,
 
 
         splitNewTypeRepCo_maybe, decomposeCo,
 

@@ -34,31 +37,18 @@ module Coercion (
 #include "HsVersions.h"
 
 import TypeRep
 #include "HsVersions.h"
 
 import TypeRep

-import Type      ( Type, Kind, PredType, substTyWith, mkAppTy, mkForAllTy,
-                    mkFunTy, splitAppTy_maybe, splitForAllTy_maybe, coreView,
-                    kindView, mkTyConApp, isCoercionKind, isEqPred, mkAppTys,
-                    coreEqType, splitAppTys, isTyVarTy, splitTyConApp_maybe,
-                    tyVarsOfType
-                  )
-import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isNewTyCon,
-                    newTyConRhs, newTyConCo, 
-                    isCoercionTyCon, isCoercionTyCon_maybe )
-import Var       ( Var, TyVar, isTyVar, tyVarKind )
-import VarSet     ( elemVarSet )
-import Name       ( BuiltInSyntax(..), Name, mkWiredInName, tcName )
-import OccName    ( mkOccNameFS )
-import PrelNames  ( symCoercionTyConKey, 
-                    transCoercionTyConKey, leftCoercionTyConKey,
-                    rightCoercionTyConKey, instCoercionTyConKey, 
-                    unsafeCoercionTyConKey, gHC_PRIM
-                  )
-import Util       ( lengthIs, snocView )
-import Unique     ( hasKey )
-import BasicTypes ( Arity )
+import Type
+import TyCon
+import Var hiding (isCoVar)
+import Name
+import OccName
+import PrelNames
+import Util
+import Unique
+import BasicTypes

 import Outputable
 
 
 import Outputable
 
 

-

 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]
 ------------------------------
 decomposeCo :: Arity -> Coercion -> [Coercion]
 -- (decomposeCo 3 c) = [right (left (left c)), right (left c), right c]

@@ -110,8 +100,8 @@ type CoercionKind = Kind    -- A CoercionKind is always of form (ty1 :=: ty2)
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)

-coercionKind (TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
-                         | otherwise = let t = (TyVarTy a) in (t, t)
+coercionKind ty@(TyVarTy a) | isCoVar a = splitCoercionKind (tyVarKind a)
+                            | otherwise = (ty, ty)

 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in
 coercionKind (AppTy ty1 ty2) 
   = let (t1, t2) = coercionKind ty1
         (s1, s2) = coercionKind ty2 in

@@ -119,10 +109,11 @@ coercionKind (AppTy ty1 ty2)
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
     -- CoercionTyCons carry their kinding rule, so we use it here
 coercionKind (TyConApp tc args)
   | Just (ar, rule) <- isCoercionTyCon_maybe tc 
     -- CoercionTyCons carry their kinding rule, so we use it here

-  = if length args >= ar 
-    then splitCoercionKind (rule args)
-    else pprPanic ("arity/arguments mismatch in coercionKind:") 
-             (ppr ar $$ ppr tc <+> ppr args)
+  = ASSERT( length args >= ar )        -- Always saturated
+    let (ty1,ty2)    = rule (take ar args)     -- Apply the rule to the right number of args
+       (tys1, tys2) = coercionKinds (drop ar args)
+    in (mkAppTys ty1 tys1, mkAppTys ty2 tys2)
+

   | otherwise
   = let (lArgs, rArgs) = coercionKinds args in
     (TyConApp tc lArgs, TyConApp tc rArgs)
   | otherwise
   = let (lArgs, rArgs) = coercionKinds args in
     (TyConApp tc lArgs, TyConApp tc rArgs)

@@ -287,43 +278,34 @@ mkUnsafeCoercion ty1 ty2
 
 
 -- See note [Newtype coercions] in TyCon
 
 
 -- See note [Newtype coercions] in TyCon

-mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
-mkNewTypeCoercion name tycon tvs rhs_ty 
-  = ASSERT (length tvs == tyConArity tycon)
-    mkCoercionTyCon name co_con_arity (mkKindingFun rule)
+mkNewTypeCoercion :: Name -> TyCon -> ([TyVar], Type) -> TyCon
+mkNewTypeCoercion name tycon (tvs, rhs_ty)
+  = mkCoercionTyCon name co_con_arity rule

   where
   where

-    rule args = (TyConApp tycon tys, substTyWith tvs_eta tys rhs_eta, rest)
-        where
-          tys  = take co_con_arity args
-          rest = drop co_con_arity args
-
-      -- if the rhs_ty is a type application and it has a tail equal to a tail
-      -- of the tvs, then we eta-contract the type of the coercion
-    rhs_args = let (ty, ty_args) = splitAppTys rhs_ty in ty_args
-
-    n_eta_tys = count_eta (reverse rhs_args) (reverse tvs)
-
-    count_eta ((TyVarTy tv):rest_ty) (tv':rest_tv)
-      | tv == tv' && (not $ any (elemVarSet tv . tyVarsOfType) rest_ty)
-                  -- if the last types are the same, and not free anywhere else
-                  -- then eta contract
-      = 1 + (count_eta rest_ty rest_tv)
-      | otherwise -- don't 
-      = 0
-    count_eta _ _ = 0
-     
-
-    eqVar (TyVarTy tv) tv' = tv == tv'
-    eqVar _            _   = False
+    co_con_arity = length tvs

 
 

-    co_con_arity = (tyConArity tycon) - n_eta_tys
+    rule args = ASSERT( co_con_arity == length args )
+               (TyConApp tycon args, substTyWith tvs args rhs_ty)

 
 

-    tvs_eta = (reverse (drop n_eta_tys (reverse tvs)))
+-- Coercion identifying a data/newtype representation type and its family
+-- instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
+-- coercion tycon built here, `F' the family tycon and `R' the (derived)
+-- representation tycon.
+--
+mkDataInstCoercion :: Name     -- unique name for the coercion tycon
+                  -> [TyVar]   -- type parameters of the coercion (`tvs')
+                  -> TyCon     -- family tycon (`F')
+                  -> [Type]    -- type instance (`ts')
+                  -> TyCon     -- representation tycon (`R')
+                  -> TyCon     -- => coercion tycon (`Co')
+mkDataInstCoercion name tvs family instTys rep_tycon
+  = mkCoercionTyCon name coArity rule
+  where
+    coArity = length tvs
+    rule args = (substTyWith tvs args $                     -- with sigma = [tys/tvs],
+                  TyConApp family instTys,          --       sigma (F ts)
+                TyConApp rep_tycon args)            --   :=: R tys

 
 

-    rhs_eta
-      | (ty, ty_args) <- splitAppTys rhs_ty
-      = mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
- 

 --------------------------------------
 -- Coercion Type Constructors...
 
 --------------------------------------
 -- Coercion Type Constructors...
 

@@ -333,14 +315,6 @@ mkNewTypeCoercion name tycon tvs rhs_ty
 --    sym d :: p2=q2
 --    sym e :: p3=q3
 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)
 --    sym d :: p2=q2
 --    sym e :: p3=q3
 -- then ((sym c) (sym d) (sym e)) :: (p1 p2 p3)=(q1 q2 q3)

---
--- (mkKindingFun f) is given the args [c, sym d, sym e]
-mkKindingFun :: ([Type] -> (Type, Type, [Type])) -> [Type] -> Kind
-mkKindingFun f args = 
-  let (ty1, ty2, rest) = f args in 
-  let (argtys1, argtys2) = unzip (map coercionKind rest) in
-  mkCoKind (mkAppTys ty1 argtys1) (mkAppTys ty2 argtys2)
-        

 
 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 -- Each coercion TyCon is built with the special CoercionTyCon record and
 
 symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, instCoercionTyCon :: TyCon
 -- Each coercion TyCon is built with the special CoercionTyCon record and

@@ -348,33 +322,34 @@ symCoercionTyCon, transCoercionTyCon, leftCoercionTyCon, rightCoercionTyCon, ins
 -- by any TyConApp in which they are applied, however they may also be over
 -- applied (see example above) and the kinding function must deal with this.
 symCoercionTyCon = 
 -- by any TyConApp in which they are applied, however they may also be over
 -- applied (see example above) and the kinding function must deal with this.
 symCoercionTyCon = 

-  mkCoercionTyCon symCoercionTyConName 1 (mkKindingFun flipCoercionKindOf)
+  mkCoercionTyCon symCoercionTyConName 1 flipCoercionKindOf

   where
   where

-    flipCoercionKindOf (co:rest) = (ty2, ty1, rest)
+    flipCoercionKindOf (co:rest) = ASSERT( null rest ) (ty2, ty1)

        where
          (ty1, ty2) = coercionKind co
 
 transCoercionTyCon = 
        where
          (ty1, ty2) = coercionKind co
 
 transCoercionTyCon = 

-  mkCoercionTyCon transCoercionTyConName 2 (mkKindingFun composeCoercionKindsOf)
+  mkCoercionTyCon transCoercionTyConName 2 composeCoercionKindsOf

   where
   where

-    composeCoercionKindsOf (co1:co2:rest) = 
+    composeCoercionKindsOf (co1:co2:rest)
+      = ASSERT( null rest )

         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")
         WARN( not (r1 `coreEqType` a2), text "Strange! Type mismatch in trans coercion, probably a bug")

-        (a1, r2, rest)
+        (a1, r2)

       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
 leftCoercionTyCon =
       where
         (a1, r1) = coercionKind co1
         (a2, r2) = coercionKind co2 
 
 leftCoercionTyCon =

-  mkCoercionTyCon leftCoercionTyConName 1 (mkKindingFun leftProjectCoercionKindOf)
+  mkCoercionTyCon leftCoercionTyConName 1 leftProjectCoercionKindOf

   where
   where

-    leftProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    leftProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)

       where
         (ty1,ty2) = fst (splitCoercionKindOf co)
 
 rightCoercionTyCon =
       where
         (ty1,ty2) = fst (splitCoercionKindOf co)
 
 rightCoercionTyCon =

-  mkCoercionTyCon rightCoercionTyConName 1 (mkKindingFun rightProjectCoercionKindOf)
+  mkCoercionTyCon rightCoercionTyConName 1 rightProjectCoercionKindOf

   where
   where

-    rightProjectCoercionKindOf (co:rest) = (ty1, ty2, rest)
+    rightProjectCoercionKindOf (co:rest) = ASSERT( null rest ) (ty1, ty2)

       where
         (ty1,ty2) = snd (splitCoercionKindOf co)
 
       where
         (ty1,ty2) = snd (splitCoercionKindOf co)
 

@@ -390,25 +365,26 @@ splitCoercionKindOf co
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 
 instCoercionTyCon 
   = ((ty_fun1, ty_fun2),(ty_arg1, ty_arg2))
 
 instCoercionTyCon 

-  =  mkCoercionTyCon instCoercionTyConName 2 (mkKindingFun instCoercionKind)
+  =  mkCoercionTyCon instCoercionTyConName 2 instCoercionKind

   where
     instantiateCo t s =
       let Just (tv, ty) = splitForAllTy_maybe t in
       substTyWith [tv] [s] ty
 
   where
     instantiateCo t s =
       let Just (tv, ty) = splitForAllTy_maybe t in
       substTyWith [tv] [s] ty
 

-    instCoercionKind (co1:ty:rest) = (instantiateCo t1 ty, instantiateCo t2 ty, rest)
+    instCoercionKind (co1:ty:rest) = ASSERT( null rest )
+                                    (instantiateCo t1 ty, instantiateCo t2 ty)

       where (t1, t2) = coercionKind co1
 
 unsafeCoercionTyCon 
       where (t1, t2) = coercionKind co1
 
 unsafeCoercionTyCon 

-  = mkCoercionTyCon unsafeCoercionTyConName 2 (mkKindingFun unsafeCoercionKind)
+  = mkCoercionTyCon unsafeCoercionTyConName 2 unsafeCoercionKind

   where
   where

-   unsafeCoercionKind (ty1:ty2:rest) = (ty1,ty2,rest) 
+   unsafeCoercionKind (ty1:ty2:rest) = ASSERT( null rest ) (ty1,ty2) 

         
 --------------------------------------
 -- ...and their names
 
 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)
         
 --------------------------------------
 -- ...and their names
 
 mkCoConName occ key coCon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ)

-                            key Nothing (ATyCon coCon) BuiltInSyntax
+                            key (ATyCon coCon) BuiltInSyntax

 
 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon
 
 transCoercionTyConName = mkCoConName FSLIT("trans") transCoercionTyConKey transCoercionTyCon
 symCoercionTyConName   = mkCoConName FSLIT("sym") symCoercionTyConKey symCoercionTyCon

@@ -427,7 +403,7 @@ splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
 splitNewTypeRepCo_maybe ty 
   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)
 splitNewTypeRepCo_maybe ty 
   | Just ty' <- coreView ty = splitNewTypeRepCo_maybe ty'
 splitNewTypeRepCo_maybe (TyConApp tc tys)

-  | isNewTyCon tc 
+  | isClosedNewTyCon tc 

   = ASSERT( tys `lengthIs` tyConArity tc )     -- splitNewTypeRepCo_maybe only be applied 
                                                 --     to *types* (of kind *)
         case newTyConRhs tc of
   = ASSERT( tys `lengthIs` tyConArity tc )     -- splitNewTypeRepCo_maybe only be applied 
                                                 --     to *types* (of kind *)
         case newTyConRhs tc of

@@ -435,6 +411,6 @@ splitNewTypeRepCo_maybe (TyConApp tc tys)
               ASSERT( length tvs == length tys )
              Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
   where
               ASSERT( length tvs == length tys )
              Just (substTyWith tvs tys rep_ty, mkTyConApp co_con tys)
   where

-    co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo tc)
+    co_con = maybe (pprPanic "splitNewTypeRepCo_maybe" (ppr tc)) id (newTyConCo_maybe tc)

 splitNewTypeRepCo_maybe other = Nothing
 \end{code}
 splitNewTypeRepCo_maybe other = Nothing
 \end{code}