- -- Split against the family tycon if the pattern constructor
- -- belongs to a family instance tycon.
- boxySplitTyConAppWithFamily tycon pat_ty =
- traceTc traceMsg >>
- case tyConFamInst_maybe tycon of
- Nothing ->
- do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp tycon pat_ty
- ; return (scrutinee_arg_tys, coi1, pat_ty)
- }
- Just (fam_tycon, instTys) ->
- do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp fam_tycon pat_ty
- ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
- ; let instTys' = substTys subst instTys
- ; cois <- boxyUnifyList instTys' scrutinee_arg_tys
- ; let coi = if isIdentityCoI coi1
- then -- pat_ty was splittable
- -- => boxyUnifyList had real work to do
- mkTyConAppCoI fam_tycon instTys' cois
- else -- pat_ty was not splittable
- -- => scrutinee_arg_tys are fresh tvs and
- -- boxyUnifyList just instantiated those
- coi1
- ; return (freshTvs, coi, mkTyConApp fam_tycon instTys')
- -- this is /= pat_ty
- -- iff cois is non-trivial
- }
- where
- traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
- ppr tycon <+> ppr pat_ty
- , text " family instance:" <+>
- ppr (tyConFamInst_maybe tycon)
- ]
-
- -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
- -- pattern if the tycon is an instance of a family.
- --
- unwrapFamInstScrutinee :: TyCon -> [Type] -> Type -> Pat Id -> Pat Id
- unwrapFamInstScrutinee tycon args unwrap_ty pat
- | Just co_con <- tyConFamilyCoercion_maybe tycon
--- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by
- -- the desugarer
- -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
- -- coercion is not the identity; mkCoPat is inconvenient as it
- -- wants a located pattern.
- = CoPat (WpCast $ mkTyConApp co_con args) -- co fam ty to repr ty
- (pat {pat_ty = mkTyConApp tycon args}) -- representation type
- unwrap_ty -- family inst type
- | otherwise
- = pat
+ (tvs, theta, tau) = tcSplitSigmaTy pat_ty
+
+----------------------------
+matchExpectedConTy :: TyCon -- The TyCon that this data
+ -- constructor actually returns
+ -> TcRhoType -- The type of the pattern
+ -> TcM (CoercionI, [TcSigmaType])
+-- See Note [Matching constructor patterns]
+-- Returns a coercion : T ty1 ... tyn ~ pat_ty
+-- This is the same way round as matchExpectedListTy etc
+-- but the other way round to matchExpectedPatTy
+matchExpectedConTy data_tc pat_ty
+ | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
+ -- Comments refer to Note [Matching constructor patterns]
+ -- co_tc :: forall a. T [a] ~ T7 a
+ = do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc)
+ -- tys = [ty1,ty2]
+
+ ; coi1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
+ -- coi1 : T (ty1,ty2) ~ pat_ty
+
+ ; let coi2 = ACo (mkTyConApp co_tc tys)
+ -- coi2 : T (ty1,ty2) ~ T7 ty1 ty2
+
+ ; return (mkTransCoI (mkSymCoI coi2) coi1, tys) }
+
+ | otherwise
+ = matchExpectedTyConApp data_tc pat_ty
+ -- coi : T tys ~ pat_ty
+\end{code}
+
+Noate [
+Note [Matching constructor patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
+
+ * In the simple case, pat_ty = tc tys
+
+ * If pat_ty is a polytype, we want to instantiate it
+ This is like part of a subsumption check. Eg
+ f :: (forall a. [a]) -> blah
+ f [] = blah
+
+ * In a type family case, suppose we have
+ data family T a
+ data instance T (p,q) = A p | B q
+ Then we'll have internally generated
+ data T7 p q = A p | B q
+ axiom coT7 p q :: T (p,q) ~ T7 p q
+
+ So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
+ coi = coi2 . coi1 : T7 t ~ pat_ty
+ coi1 : T (ty1,ty2) ~ pat_ty
+ coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
+
+ For families we do all this matching here, not in the unifier,
+ because we never want a whisper of the data_tycon to appear in
+ error messages; it's a purely internal thing