Fixed uninitialised FunBind fun_tick field
[ghc-hetmet.git] / compiler / types / Coercion.lhs
index 1dbd7f3..e17d0b0 100644 (file)
@@ -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. 
@@ -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, mkTyVarTys
-                  )
-import TyCon      ( TyCon, tyConArity, mkCoercionTyCon, isClosedNewTyCon,
-                    newTyConRhs, newTyConCo_maybe, 
-                    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
+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]
@@ -101,17 +91,14 @@ splitCoercionKind_maybe co | Just co' <- kindView co = splitCoercionKind_maybe c
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 splitCoercionKind_maybe other = Nothing
 
 splitCoercionKind_maybe (PredTy (EqPred ty1 ty2)) = Just (ty1, ty2)
 splitCoercionKind_maybe other = Nothing
 
-isCoVar :: Var -> Bool
-isCoVar tv = isTyVar tv && isCoercionKind (tyVarKind tv)
-
 type Coercion     = Type
 type CoercionKind = Kind       -- A CoercionKind is always of form (ty1 :=: ty2)
 
 coercionKind :: Coercion -> (Type, Type)
 --     c :: (t1 :=: t2)
 -- Then (coercionKind c) = (t1,t2)
 type Coercion     = Type
 type CoercionKind = Kind       -- A CoercionKind is always of form (ty1 :=: ty2)
 
 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 +106,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,42 +275,14 @@ 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
-
-    tvs_eta = (reverse (drop n_eta_tys (reverse tvs)))
-
-    rhs_eta
-      | (ty, ty_args) <- splitAppTys rhs_ty
-      = mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
+    rule args = ASSERT( co_con_arity == length args )
+               (TyConApp tycon args, substTyWith tvs args rhs_ty)
 
 -- 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 identifying a data/newtype representation type and its family
 -- instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
@@ -336,17 +296,12 @@ mkDataInstCoercion :: Name        -- unique name for the coercion tycon
                   -> TyCon     -- representation tycon (`R')
                   -> TyCon     -- => coercion tycon (`Co')
 mkDataInstCoercion name tvs family instTys rep_tycon
                   -> TyCon     -- representation tycon (`R')
                   -> TyCon     -- => coercion tycon (`Co')
 mkDataInstCoercion name tvs family instTys rep_tycon
-  = mkCoercionTyCon name coArity (mkKindingFun rule)
+  = mkCoercionTyCon name coArity rule
   where
     coArity = length tvs
   where
     coArity = length tvs
-
-    rule args = (substTyWith tvs tys $              -- with sigma = [tys/tvs],
+    rule args = (substTyWith tvs args $                     -- with sigma = [tys/tvs],
                   TyConApp family instTys,          --       sigma (F ts)
                   TyConApp family instTys,          --       sigma (F ts)
-                TyConApp rep_tycon tys,             --   :=: R tys
-                rest)                               -- surplus arguments
-      where
-        tys  = take coArity args
-        rest = drop coArity args
+                TyConApp rep_tycon args)            --   :=: R tys
 
 --------------------------------------
 -- Coercion Type Constructors...
 
 --------------------------------------
 -- Coercion Type Constructors...
@@ -357,14 +312,6 @@ mkDataInstCoercion name tvs family instTys rep_tycon
 --    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
@@ -372,33 +319,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)
 
@@ -414,25 +362,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