TcPat: Typechecking patterns
\begin{code}
-module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit,
+module TcPat ( tcLetPat, tcPat, tcPats, tcOverloadedLit,
addDataConStupidTheta, badFieldCon, polyPatSig ) where
#include "HsVersions.h"
import DataCon
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
+import DynFlags ( DynFlag( Opt_GADTs ) )
import SrcLoc
import ErrUtils
import Util
; return (pat', res) }
-----------------
-tcLamPats :: [LPat Name] -- Patterns,
- -> [BoxySigmaType] -- and their types
- -> BoxyRhoType -- Result type,
- -> (BoxyRhoType -> TcM a) -- and the checker for the body
- -> TcM ([LPat TcId], a)
+tcPats :: HsMatchContext Name
+ -> [LPat Name] -- Patterns,
+ -> [BoxySigmaType] -- and their types
+ -> BoxyRhoType -- Result type,
+ -> (BoxyRhoType -> TcM a) -- and the checker for the body
+ -> TcM ([LPat TcId], a)
-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
-- 3. Check the body
-- 4. Check that no existentials escape
-tcLamPats pats tys res_ty thing_inside
- = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
+tcPats ctxt pats tys res_ty thing_inside
+ = tc_lam_pats (APat ctxt) (zipEqual "tcLamPats" pats tys)
res_ty thing_inside
-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
+tcPat :: HsMatchContext Name
+ -> LPat Name -> BoxySigmaType
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given
+ -- its result type
+ -> TcM (LPat TcId, a)
+tcPat ctxt = tc_lam_pat (APat ctxt)
tc_lam_pat :: PatCtxt -> LPat Name -> BoxySigmaType -> BoxyRhoType
-> (BoxyRhoType -> TcM a) -> TcM (LPat TcId, a)
; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty))
; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
if (pat_eqs pstate' && (not $ isRigidTy res_ty))
- then nonRigidResult res_ty
+ then nonRigidResult ctxt res_ty
else thing_inside res_ty }
; let tys = map snd pat_ty_prs
}
data PatCtxt
- = LamPat
- | ProcPat -- The pattern in (proc pat -> ...)
- -- see Note [Arrows and patterns]
+ = APat (HsMatchContext Name)
| LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
+notProcPat :: PatCtxt -> Bool
+notProcPat (APat ProcExpr) = False
+notProcPat _ = True
+
patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
patSigCtxt _ = LamPatSigCtxt
-- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
-- Check no existentials
- ; if (null pat_tvs) then return ()
- else lazyPatErr lpat pat_tvs
+ ; unless (null pat_tvs) $ lazyPatErr lpat pat_tvs
+
+ -- Check there are no unlifted types under the lazy pattern
+ ; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
+ lazyUnliftedPatErr lpat
-- Check that the pattern has a lifted type
; pat_tv <- newBoxyTyVar liftedTypeKind
-- 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 (isIdentityCoI 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
else do -- The general case, with existential, and local equality
-- constraints
- { checkTc (case pat_ctxt pstate of { ProcPat -> False; _ -> True })
+ { checkTc (notProcPat (pat_ctxt pstate))
(existentialProcPat data_con)
+ -- See Note [Arrows and patterns]
-- Need to test for rigidity if *any* constraints in theta as class
-- constraints may have superclass equality constraints. However,
-- 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))
+ ; gadts_on <- doptM 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
+
+ ; unless no_equalities $ checkTc (isRigidTy pat_ty) $
+ nonRigidMatch (pat_ctxt pstate) 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 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:" <+>
-- 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)
-- 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 "I can't handle pattern bindings for existential or GADT data constructors.",
text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
text "In the binding group for"])
4 (ppr pat)
= 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
lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
lazyPatErr _ tvs
= failWithTc $
- hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
+ hang (ptext (sLit "A lazy (~) pattern cannot match existential or GADT data constructors"))
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"))
+lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
+lazyUnliftedPatErr pat
+ = failWithTc $
+ hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types"))
+ 2 (ppr pat)
-nonRigidResult :: Type -> TcM a
-nonRigidResult res_ty
+nonRigidMatch :: PatCtxt -> DataCon -> SDoc
+nonRigidMatch ctxt con
+ = hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
+ 2 (ptext (sLit "Probable solution: add a type signature for") <+> what ctxt)
+ where
+ what (APat (FunRhs f _)) = quotes (ppr f)
+ what (APat CaseAlt) = ptext (sLit "the scrutinee of the case expression")
+ what (APat LambdaExpr ) = ptext (sLit "the lambda expression")
+ what (APat (StmtCtxt _)) = ptext (sLit "the right hand side of a do/comprehension binding")
+ what _other = ptext (sLit "something")
+
+nonRigidResult :: PatCtxt -> Type -> TcM a
+nonRigidResult ctxt res_ty
= do { env0 <- tcInitTidyEnv
; let (env1, res_ty') = tidyOpenType env0 res_ty
msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
<+> quotes (ppr res_ty'))
- 2 (ptext (sLit "Solution: add a type signature"))
+ 2 (ptext (sLit "Solution: add a type signature for")
+ <+> what ctxt )
; failWithTcM (env1, msg) }
+ where
+ what (APat (FunRhs f _)) = quotes (ppr f)
+ what (APat CaseAlt) = ptext (sLit "the entire case expression")
+ what (APat LambdaExpr) = ptext (sLit "the lambda exression")
+ what (APat (StmtCtxt _)) = ptext (sLit "the entire do/comprehension expression")
+ what _other = ptext (sLit "something")
\end{code}
projects / ghc-hetmet.git / blobdiff