+
+%************************************************************************
+%* *
+ Looking up a family instance
+%* *
+%************************************************************************
+
+\begin{code}
+topNormaliseType :: FamInstEnvs
+ -> Type
+ -> Maybe (Coercion, Type)
+
+-- Get rid of *outermost* (or toplevel) type functions by rewriting them
+-- By "outer" we mean that toplevelNormaliseType guarantees to return
+-- a type that does not have a reducible redex (F ty1 .. tyn) as its
+-- outermost form. It *can* return something like (Maybe (F ty)), where
+-- (F ty) is a redex.
+
+topNormaliseType env ty
+ | Just ty' <- tcView ty = topNormaliseType env ty'
+
+topNormaliseType env ty@(TyConApp tc tys)
+ | isOpenTyCon tc
+ , (ACo co, ty) <- normaliseType env ty
+ = Just (co, ty)
+
+topNormaliseType env ty
+ = Nothing
+
+
+normaliseType :: FamInstEnvs -- environment with family instances
+ -> Type -- old type
+ -> (CoercionI,Type) -- (coercion,new type), where
+ -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating all type-function redexes
+
+normaliseType env ty
+ | Just ty' <- coreView ty = normaliseType env ty'
+
+normaliseType env ty@(TyConApp tyCon tys)
+ = let -- First normalise the arg types
+ (cois, ntys) = mapAndUnzip (normaliseType env) tys
+ tycon_coi = mkTyConAppCoI tyCon ntys cois
+ in -- Now try the top-level redex
+ case lookupFamInstEnv env tyCon ntys of
+ -- A matching family instance exists
+ [(fam_inst, tys)] -> (fix_coi, nty)
+ where
+ rep_tc = famInstTyCon fam_inst
+ co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+ co = mkTyConApp co_tycon tys
+ first_coi = mkTransCoI tycon_coi (ACo co)
+ (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
+ fix_coi = mkTransCoI first_coi rest_coi
+
+ -- No unique matching family instance exists;
+ -- we do not do anything
+ other -> (tycon_coi, TyConApp tyCon ntys)
+
+ where
+
+normaliseType env ty@(AppTy ty1 ty2)
+ = let (coi1,nty1) = normaliseType env ty1
+ (coi2,nty2) = normaliseType env ty2
+ in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+normaliseType env ty@(FunTy ty1 ty2)
+ = let (coi1,nty1) = normaliseType env ty1
+ (coi2,nty2) = normaliseType env ty2
+ in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+normaliseType env ty@(ForAllTy tyvar ty1)
+ = let (coi,nty1) = normaliseType env ty1
+ in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseType env ty@(NoteTy note ty1)
+ = let (coi,nty1) = normaliseType env ty1
+ in (mkNoteTyCoI note coi,NoteTy note nty1)
+normaliseType env ty@(TyVarTy _)
+ = (IdCo,ty)
+normaliseType env (PredTy predty)
+ = normalisePred env predty
+
+normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normalisePred env (ClassP cls tys)
+ = let (cois,tys') = mapAndUnzip (normaliseType env) tys
+ in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+normalisePred env (IParam ipn ty)
+ = let (coi,ty') = normaliseType env ty
+ in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+normalisePred env (EqPred ty1 ty2)
+ = let (coi1,ty1') = normaliseType env ty1
+ (coi2,ty2') = normaliseType env ty2
+ in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+\end{code}