X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=984b2e5481b9e9d5f6547c93a1ab2a0b6c96264b;hb=f5209837011fe1ff46e94d7d807c16f2fd6cb0e2;hp=2e865835b66bfedbecceb0616b6c65fc66e3dac7;hpb=6344b1506042f6e150c1b105c6696f3d75a5eb66;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 2e86583..984b2e5 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -422,7 +422,10 @@ tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside -- 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) } @@ -565,7 +568,7 @@ the split arguments for the representation tycon :R123Map as {Int, c, w} 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 @@ -591,7 +594,7 @@ to express the local scope of GADT refinements. \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 @@ -608,18 +611,16 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside -- 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 @@ -655,7 +656,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside -- 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) @@ -665,8 +666,8 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside 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 @@ -688,12 +689,26 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats 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:" <+> @@ -705,8 +720,8 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside -- 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 @@ -715,11 +730,10 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside -- 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) @@ -997,6 +1011,10 @@ polyPatSig sig_ty = 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