TcPat: Typechecking patterns
\begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit,
addDataConStupidTheta, badFieldCon, polyPatSig ) where
import TcEnv
import TcMType
import TcType
+import VarEnv
import VarSet
import TcUnify
import TcHsType
import StaticFlags
import TyCon
import DataCon
-import DynFlags
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
import SrcLoc
= tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
res_ty thing_inside
-tcLamPat :: LPat Name -> BoxySigmaType
- -> BoxyRhoType -- Result type
- -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
- -> TcM (LPat TcId, a)
-
-tcProcPat = tc_lam_pat ProcPat
+tcLamPat, tcProcPat :: LPat Name -> BoxySigmaType
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given
+ -- its result type
+ -> TcM (LPat TcId, a)
tcLamPat = tc_lam_pat LamPat
+tcProcPat = tc_lam_pat ProcPat
+tc_lam_pat :: PatCtxt -> LPat Name -> BoxySigmaType -> BoxyRhoType
+ -> (BoxyRhoType -> TcM a) -> TcM (LPat TcId, a)
tc_lam_pat ctxt pat pat_ty res_ty thing_inside
= do { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
; return (pat', thing) }
-- f (C g) x = g x
-- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
-tcCheckExistentialPat pats [] pat_tys body_ty
+tcCheckExistentialPat _ [] _ _
= return () -- Short cut for case when there are no existentials
tcCheckExistentialPat pats ex_tvs pat_tys body_ty
patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
-patSigCtxt other = LamPatSigCtxt
+patSigCtxt _ = LamPatSigCtxt
\end{code}
; return (res, binds) }
-------------------
+unBoxPatBndrType :: BoxyType -> Name -> TcM TcType
unBoxPatBndrType ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
+
+unBoxWildCardType :: BoxyType -> TcM TcType
unBoxWildCardType ty = unBoxArgType ty (ptext (sLit "A wild-card pattern"))
+
+unBoxViewPatType :: BoxyType -> Pat Name -> TcM TcType
unBoxViewPatType ty pat = unBoxArgType ty (ptext (sLit "The view pattern") <+> ppr pat)
unBoxArgType :: BoxyType -> SDoc -> TcM TcType
-- 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) }
-tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+tc_pat _ pat@(TypePat _) _ _
= failWithTc (badTypePat pat)
------------------------
------------------------
-- Data constructors
-tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
+tc_pat pstate (ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
= do { data_con <- tcLookupDataCon con_name
; let tycon = dataConTyCon data_con
; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
; coi <- boxyUnify lit_ty pat_ty
-- coi is of kind: lit_ty ~ pat_ty
; res <- thing_inside pstate
- ; span <- getSrcSpanM
-- pattern coercions have to
-- be of kind: pat_ty ~ lit_ty
-- hence, sym coi
------------------------
-- Overloaded patterns: n, and n+k
-tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
+tc_pat pstate (NPat over_lit mb_neg eq) pat_ty thing_inside
= do { let orig = LiteralOrigin over_lit
; lit' <- tcOverloadedLit orig over_lit pat_ty
; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
; res <- thing_inside pstate
; return (NPat lit' mb_neg' eq', [], res) }
-tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
+tc_pat pstate (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
= do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
; let pat_ty' = idType bndr_id
orig = LiteralOrigin lit
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
else do -- The general case, with existential, and local equality
-- constraints
- { checkTc (case pat_ctxt pstate of { ProcPat -> False; other -> True })
+ { checkTc (case pat_ctxt pstate of { ProcPat -> False; _ -> True })
(existentialProcPat data_con)
-- Need to test for rigidity if *any* constraints in theta as class
-- 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)
where
con_arity = dataConSourceArity data_con
-tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
- = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
-
tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
= do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
; return (RecCon (HsRecFields rpats' dd), tvs, res) }
-- The origin should always report "occurrence of C"
-- even when C occurs in a pattern
stupid_theta = dataConStupidTheta data_con
- tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
+ tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
+ -- NB: inst_tys can be longer than the univ tyvars
+ -- because the constructor might have existentials
inst_theta = substTheta tenv stupid_theta
\end{code}
-----------------------------------------------
+existentialExplode :: LPat Name -> SDoc
existentialExplode pat
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existentially-quantified constructors.",
text "In the binding group for"])
4 (ppr pat)
+sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
= do { pat_tys' <- mapM zonkTcType pat_tys
; body_ty' <- zonkTcType body_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
existentialProcPat :: DataCon -> SDoc
= hang (ptext (sLit "Illegal constructor") <+> quotes (ppr con) <+> ptext (sLit "in a 'proc' pattern"))
2 (ptext (sLit "Proc patterns cannot use existentials or GADTs"))
-lazyPatErr pat tvs
+lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
+lazyPatErr _ tvs
= failWithTc $
hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
2 (vcat (map pprSkolTvBinding tvs))
+nonRigidMatch :: DataCon -> SDoc
nonRigidMatch con
= hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
2 (ptext (sLit "Solution: add a type signature"))
+nonRigidResult :: Type -> TcM a
nonRigidResult res_ty
= do { env0 <- tcInitTidyEnv
; let (env1, res_ty') = tidyOpenType env0 res_ty
<+> quotes (ppr res_ty'))
2 (ptext (sLit "Solution: add a type signature"))
; failWithTcM (env1, msg) }
-
-inaccessibleAlt msg
- = hang (ptext (sLit "Inaccessible case alternative:")) 2 msg
\end{code}
projects / ghc-hetmet.git / blobdiff