-
-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 (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)