-- Type signatures in patterns
-- See Note [Pattern coercions] below
tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
- = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
+ = do { (inner_ty, tv_binds, coi) <- tcPatSig (patSigCtxt pstate) sig_ty
+ pat_ty
+ ; unless (isIdentityCoercion coi) $
+ failWithTc (badSigPat pat_ty)
; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
tc_lpat pat inner_ty pstate thing_inside
; return (SigPatOut pat' inner_ty, tvs, res) }
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
- Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+ Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
moving between representation and family type into account. To produce type
correct Core, this coercion needs to be used to case the type of the scrutinee
\begin{code}
-- Running example:
--- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
-- with scrutinee of type (T ty)
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
-- Instantiate the constructor type variables [a->ty]
-- This may involve doing a family-instance coercion, and building a
-- wrapper
- ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
+ ; (ctxt_res_tys, coi, unwrap_ty) <- boxySplitTyConAppWithFamily tycon
+ pat_ty
; let sym_coi = mkSymCoI coi -- boxy split coercion oriented wrongly
pat_ty' = mkTyConApp tycon ctxt_res_tys
-- pat_ty' /= pat_ty iff coi /= IdCo
wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
where
- uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
-
- ; traceTc $ case sym_coi of
- IdCo -> text "sym_coi:IdCo"
- ACo co -> text "sym_coi: ACoI" <+> ppr co
+ uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys
+ unwrap_ty res_pat
-- Add the stupid theta
; addDataConStupidTheta data_con ctxt_res_tys
-- ex_tvs was non-null.
-- ; unless (null theta') $
-- FIXME: AT THE MOMENT WE CHEAT! We only perform the rigidity test
- -- if we explicit or implicit (by a GADT def) have equality
+ -- if we explicitly or implicitly (by a GADT def) have equality
-- constraints.
; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
theta' = substTheta tenv (eq_preds ++ full_theta)
pstate' | no_equalities = pstate
| otherwise = pstate { pat_eqs = True }
- ; unless no_equalities (checkTc (isRigidTy pat_ty)
- (nonRigidMatch data_con))
+ ; unless no_equalities $
+ checkTc (isRigidTy pat_ty) (nonRigidMatch data_con)
; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
boxySplitTyConAppWithFamily tycon pat_ty =
traceTc traceMsg >>
case tyConFamInst_maybe tycon of
- Nothing -> boxySplitTyConApp tycon pat_ty
+ 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, coi) <- boxySplitTyConApp fam_tycon pat_ty
+ do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp fam_tycon pat_ty
; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
- ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
- ; return (freshTvs, coi)
+ ; let instTys' = substTys subst instTys
+ ; cois <- boxyUnifyList instTys' scrutinee_arg_tys
+ ; let coi = if isIdentityCoercion 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:" <+>
-- 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] -> Pat Id -> Pat Id
- unwrapFamInstScrutinee tycon args pat
+ 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
-- wants a located pattern.
= CoPat (WpCast $ mkTyConApp co_con args) -- co fam ty to repr ty
(pat {pat_ty = mkTyConApp tycon args}) -- representation type
- pat_ty -- family inst type
+ unwrap_ty -- family inst type
| otherwise
= pat
-
tcConArgs :: DataCon -> [TcSigmaType]
-> Checker (HsConPatDetails Name) (HsConPatDetails Id)
= hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
2 (ppr sig_ty)
+badSigPat :: TcType -> SDoc
+badSigPat pat_ty = ptext (sLit "Pattern signature must exactly match:") <+>
+ ppr pat_ty
+
badTypePat :: Pat Name -> SDoc
badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
projects / ghc-hetmet.git / blobdiff