- -- 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
+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;