X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FFamInstEnv.lhs;h=d1a344521d722fa3d2f22b1afdb99468093e1ac5;hb=701797c3f724090508e06ded276723edfa431ab4;hp=c8a509f059c2f592ab06c01222a14f3e61ec5dd2;hpb=13cd965d80be5c25dc54534a833df39ab7aa7a12;p=ghc-hetmet.git

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index c8a509f..d1a3445 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -14,7 +14,10 @@ module FamInstEnv (
 	extendFamInstEnv, extendFamInstEnvList, 
 	famInstEnvElts, familyInstances,
 
-	lookupFamInstEnv, lookupFamInstEnvUnify
+	lookupFamInstEnv, lookupFamInstEnvUnify,
+	
+	-- Normalisation
+	toplevelNormaliseFamInst
     ) where
 
 #include "HsVersions.h"
@@ -24,7 +27,9 @@ import Unify
 import TcGadt
 import TcType
 import Type
+import TypeRep
 import TyCon
+import Coercion
 import VarSet
 import Var
 import Name
@@ -32,6 +37,8 @@ import OccName
 import SrcLoc
 import UniqFM
 import Outputable
+import Maybes
+import Util
 
 import Maybe
 \end{code}
@@ -82,7 +89,7 @@ instance Outputable FamInst where
 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})
@@ -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).
 
+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}
+type FamInstMatch = (FamInst, [Type])           -- Matching type instance
+
 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
@@ -231,7 +252,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam 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
@@ -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]
-	              -> [(TvSubst, FamInst)]
+	              -> [(FamInstMatch)]
 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
-	    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@.
@@ -294,3 +317,99 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
 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}