-tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
- -> BoxySigmaType -- Type of the pattern
- -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
- -> TcM (Pat TcId, [TcTyVar], a)
-tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
- | isVanillaDataCon data_con
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
- inst_prs = zipEqual "tcConPat" tvs ty_args
- subst = mkTopTvSubst inst_prs
- arg_tys' = substTys subst arg_tys
- unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
- not (tv `elemVarSet` arg_tvs)]
- ; mapM unBox unconstrained_ty_args -- Zap these to monotypes
- ; tcInstStupidTheta data_con ty_args
- ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
- ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
- ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs, res) }
-
- | otherwise -- GADT case
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; span <- getSrcSpanM -- The whole pattern
-
- -- Instantiate the constructor type variables and result type
- ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
- skol_info = PatSkol data_con span
- arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
- ; tvs' <- tcInstSkolTyVars skol_info tvs
- ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
-
- -- Do type refinement!
- ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys',
- text "ty-args:" <+> ppr ty_args ])
- ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args
- $ \ pstate' tv_tys' -> do
-
- -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
- -- or the tv_tys' in the call to tcInstStupidTheta
- { let tenv' = zipTopTvSubst tvs tv_tys'
- theta' = substTheta tenv' theta
- arg_tys' = substTys tenv' arg_tys -- Boxy types
-
- ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
- do { tcInstStupidTheta data_con tv_tys'
- -- The stupid-theta mentions the newly-bound tyvars, so
- -- it must live inside the getLIE, so that the
- -- tcSimplifyCheck will apply the type refinement to it
- ; tcConArgs pstate' data_con arg_pats arg_tys' thing_inside }
-
- ; dicts <- newDicts (SigOrigin skol_info) theta'
- ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
-
- ; return (ConPatOut (L con_span data_con)
- tvs' (map instToId dicts) dict_binds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs' ++ inner_tvs, res)
+-- Running example:
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
+-- with scrutinee of type (T ty)
+
+tcConPat :: PatEnv -> Located Name
+ -> TcRhoType -- Type of the pattern
+ -> HsConPatDetails Name -> TcM a
+ -> TcM (Pat TcId, a)
+tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
+ = do { data_con <- tcLookupDataCon con_name
+ ; let tycon = dataConTyCon data_con
+ -- For data families this is the representation tycon
+ (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
+ = dataConFullSig data_con
+
+ -- Instantiate the constructor type variables [a->ty]
+ -- This may involve doing a family-instance coercion,
+ -- and building a wrapper
+ ; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty
+
+ -- Add the stupid theta
+ ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
+
+ ; checkExistentials ex_tvs penv
+ ; let skol_info = case pe_ctxt penv of
+ LamPat mc -> PatSkol data_con mc
+ LetPat {} -> UnkSkol -- Doesn't matter
+ ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+ -- Get location from monad, not from ex_tvs
+
+ ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
+ -- pat_ty' is type of the actual constructor application
+ -- pat_ty' /= pat_ty iff coi /= IdCo
+
+ tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
+ (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+ arg_tys' = substTys tenv arg_tys
+ full_theta = eq_theta ++ dict_theta
+
+ ; if null ex_tvs && null eq_spec && null full_theta
+ then do { -- The common case; no class bindings etc
+ -- (see Note [Arrows and patterns])
+ (arg_pats', res) <- tcConArgs data_con arg_tys'
+ arg_pats penv thing_inside
+ ; let res_pat = ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = [], pat_dicts = [],
+ pat_binds = emptyTcEvBinds,
+ pat_args = arg_pats',
+ pat_ty = pat_ty' }
+
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
+
+ else do -- The general case, with existential,
+ -- and local equality constraints
+ { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
+ theta' = substTheta tenv (eq_preds ++ full_theta)
+ -- order is *important* as we generate the list of
+ -- dictionary binders from theta'
+ no_equalities = not (any isEqPred theta')
+
+ ; gadts_on <- xoptM Opt_GADTs
+ ; checkTc (no_equalities || gadts_on)
+ (ptext (sLit "A pattern match on a GADT requires -XGADTs"))
+ -- Trac #2905 decided that a *pattern-match* of a GADT
+ -- should require the GADT language flag
+
+ ; given <- newEvVars theta'
+ ; let free_tvs = pe_res_tvs penv
+ -- Since we have done checkExistentials,
+ -- pe_res_tvs can only be Just at this point
+ --
+ -- Nor do we need pat_ty, because we've put all the
+ -- unification variables in right at the start when
+ -- initialising the PatEnv; and the pattern itself
+ -- only adds skolems.
+
+ ; (ev_binds, (arg_pats', res))
+ <- checkConstraints skol_info free_tvs ex_tvs' given $
+ tcConArgs data_con arg_tys' arg_pats penv thing_inside
+
+ ; let res_pat = ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = ex_tvs',
+ pat_dicts = given,
+ pat_binds = ev_binds,
+ pat_args = arg_pats',
+ pat_ty = pat_ty' }
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res)