- 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
+ = (tycon_coi, TyConApp tc ntys)
+
+ where
+ -- Normalise the arg types so that they'll match
+ -- when we lookup in in the instance envt
+ (cois, ntys) = mapAndUnzip (normaliseType env) tys
+ tycon_coi = mkTyConAppCo tc cois
+
+---------------
+normaliseType :: FamInstEnvs -- environment with family instances
+ -> Type -- old type
+ -> (Coercion, Type) -- (coercion,new type), where
+ -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating *all* type-function redexes
+-- Returns with Refl if nothing happens
+
+normaliseType env ty
+ | Just ty' <- coreView ty = normaliseType env ty'
+normaliseType env (TyConApp tc tys)
+ = normaliseTcApp env tc tys
+normaliseType env (AppTy ty1 ty2)
+ = let (coi1,nty1) = normaliseType env ty1
+ (coi2,nty2) = normaliseType env ty2
+ in (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
+normaliseType env (FunTy ty1 ty2)
+ = let (coi1,nty1) = normaliseType env ty1
+ (coi2,nty2) = normaliseType env ty2
+ in (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
+normaliseType env (ForAllTy tyvar ty1)
+ = let (coi,nty1) = normaliseType env ty1
+ in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
+normaliseType _ ty@(TyVarTy _)
+ = (Refl ty,ty)
+normaliseType env (PredTy predty)
+ = normalisePred env predty
+
+---------------
+normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
+normalisePred env (ClassP cls tys)
+ = let (cos,tys') = mapAndUnzip (normaliseType env) tys
+ in (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
+normalisePred env (IParam ipn ty)
+ = let (co,ty') = normaliseType env ty
+ in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
+normalisePred env (EqPred ty1 ty2)
+ = let (co1,ty1') = normaliseType env ty1
+ (co2,ty2') = normaliseType env ty2
+ in (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')