White-space only

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

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index c8a509f..d1a3445 100644 (file)
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -14,7 +14,10 @@ module FamInstEnv (
        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 
        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 

-       lookupFamInstEnv, lookupFamInstEnvUnify
+       lookupFamInstEnv, lookupFamInstEnvUnify,
+       
+       -- Normalisation
+       toplevelNormaliseFamInst

     ) where
 
 #include "HsVersions.h"
     ) where
 
 #include "HsVersions.h"

@@ -24,7 +27,9 @@ import Unify
 import TcGadt
 import TcType
 import Type
 import TcGadt
 import TcType
 import Type

+import TypeRep

 import TyCon
 import TyCon

+import Coercion

 import VarSet
 import Var
 import Name
 import VarSet
 import Var
 import Name

@@ -32,6 +37,8 @@ import OccName
 import SrcLoc
 import UniqFM
 import Outputable
 import SrcLoc
 import UniqFM
 import Outputable

+import Maybes
+import Util

 
 import Maybe
 \end{code}
 
 import Maybe
 \end{code}

@@ -82,7 +89,7 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)

-       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst)))
+       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcSpan famInst)))

 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})

@@ -198,10 +205,24 @@ Multiple matches are only possible in case of type families (not data
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 

+We return the matching family instances and the type instance at which it
+matches.  For example, if we lookup 'T [Int]' and have a family instance
+
+  data instance T [a] = ..
+
+desugared to
+
+  data :R42T a = ..
+  coe :Co:R42T a :: T [a] ~ :R42T a
+
+we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
+

 \begin{code}
 \begin{code}

+type FamInstMatch = (FamInst, [Type])           -- Matching type instance
+

 lookupFamInstEnv :: FamInstEnvs
                 -> TyCon -> [Type]             -- What we are looking for
 lookupFamInstEnv :: FamInstEnvs
                 -> TyCon -> [Type]             -- What we are looking for

-                -> [(TvSubst, FamInst)]        -- Successful matches
+                -> [FamInstMatch]              -- Successful matches

 lookupFamInstEnv (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
 lookupFamInstEnv (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where

@@ -231,7 +252,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys

-      = (subst, item) : find rest
+      = (item, substTyVars subst (tyConTyVars tycon)) : find rest

 
         -- No match => try next
       | otherwise
 
         -- No match => try next
       | otherwise

@@ -250,7 +271,7 @@ indexed synonyms and we don't want to slow that down by needless unification.
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]

-                     -> [(TvSubst, FamInst)]
+                     -> [(FamInstMatch)]

 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where
 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
   = home_matches ++ pkg_matches
   where

@@ -286,7 +307,9 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
         case tcUnifyTys bind_fn tpl_tys tys of
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
         case tcUnifyTys bind_fn tpl_tys tys of

-           Just subst -> (subst, item) : find rest
+           Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
+                          in
+                          (item, rep_tys) : find rest

            Nothing    -> find rest
 
 -- See explanation at @InstEnv.bind_fn@.
            Nothing    -> find rest
 
 -- See explanation at @InstEnv.bind_fn@.

@@ -294,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
           | otherwise                             = BindMe
 \end{code}
 bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
           | otherwise                             = BindMe
 \end{code}

+
+--------------------------------------
+-- Normalisation 
+
+\begin{code}
+       -- get rid of TOPLEVEL type functions by rewriting them 
+       -- i.e. treating their equations as a TRS
+toplevelNormaliseFamInst :: FamInstEnvs ->
+                           Type ->
+                           (CoercionI,Type)
+toplevelNormaliseFamInst env ty
+       | Just ty' <- tcView ty = normaliseFamInst env ty'
+toplevelNormaliseFamInst env ty@(TyConApp tyCon tys)
+       | isOpenTyCon tyCon
+       = normaliseFamInst env ty
+toplevelNormaliseFamInst env ty
+       = (IdCo,ty)
+        
+
+       -- get rid of ALL type functions by rewriting them 
+       -- i.e. treating their equations as a TRS
+normaliseFamInst :: FamInstEnvs ->     -- environment with family instances
+                   Type ->             -- old type
+                   (CoercionI,Type)    -- (coercion,new type)
+normaliseFamInst env ty 
+       | Just ty' <- tcView ty = normaliseFamInst env ty' 
+normaliseFamInst env ty@(TyConApp tyCon tys) =
+       let (cois,ntys) = mapAndUnzip (normaliseFamInst env) tys
+           tycon_coi   = mkTyConAppCoI tyCon ntys cois
+           maybe_ty_co = lookupFamInst env tyCon ntys
+        in case maybe_ty_co of
+               -- a matching family instance exists
+               Just (ty',co) ->
+                       let first_coi      = mkTransCoI tycon_coi (ACo co)
+                           (rest_coi,nty) = normaliseFamInst env ty'
+                           fix_coi        = mkTransCoI first_coi rest_coi
+                       in (fix_coi,nty)
+               -- no matching family instance exists
+               -- we do not do anything
+               Nothing -> 
+                       (tycon_coi,TyConApp tyCon ntys)
+normaliseFamInst env ty@(AppTy ty1 ty2)        =
+       let (coi1,nty1) = normaliseFamInst env ty1
+           (coi2,nty2) = normaliseFamInst env ty2
+       in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+normaliseFamInst env ty@(FunTy ty1 ty2)        =
+       let (coi1,nty1) = normaliseFamInst env ty1
+           (coi2,nty2) = normaliseFamInst env ty2
+       in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+normaliseFamInst env ty@(ForAllTy tyvar ty1)   =
+       let (coi,nty1) = normaliseFamInst env ty1
+       in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseFamInst env ty@(NoteTy note ty1)      =
+       let (coi,nty1) = normaliseFamInst env ty1
+       in  (mkNoteTyCoI note coi,NoteTy note nty1)
+normaliseFamInst env ty@(TyVarTy _) =
+       (IdCo,ty)
+normaliseFamInst env (PredTy predty) =
+       normaliseFamInstPred env predty 
+
+normaliseFamInstPred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normaliseFamInstPred env (ClassP cls tys) =
+       let (cois,tys') = mapAndUnzip (normaliseFamInst env) tys
+       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+normaliseFamInstPred env (IParam ipn ty) =
+       let (coi,ty') = normaliseFamInst env ty
+       in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+normaliseFamInstPred env (EqPred ty1 ty2) =
+       let (coi1,ty1') = normaliseFamInst env ty1
+            (coi2,ty2') = normaliseFamInst env ty2
+       in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+ 
+lookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type,Coercion)
+
+-- (lookupFamInst F tys) looks for a top-level instance
+--     co : forall a. F tys' = G a
+--   (The rhs is always of form G a; see Note [The FamInst structure]
+--     in FamInst.)
+-- where we can instantiate 'a' with t to make tys'[t/a] = tys
+-- Hence   (co t) : F tys ~ G t
+-- Then we return (Just (G t, co t))
+
+lookupFamInst env tycon tys 
+  | not (isOpenTyCon tycon)            -- Dead code; fix.
+  = Nothing
+  | otherwise
+  = case lookupFamInstEnv env tycon tys of
+          [(subst, fam_inst)] -> 
+            Just (mkTyConApp rep_tc substituted_vars, mkTyConApp coercion_tycon substituted_vars)
+               where   -- NB: invariant of lookupFamInstEnv is that (tyConTyVars rep_tc)
+                       --     is in the domain of the substitution
+                 rep_tc           = famInstTyCon fam_inst
+                 coercion_tycon   = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+                 substituted_vars = substTyVars subst (tyConTyVars rep_tc)
+          other -> Nothing
+\end{code}