\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcMonoPatBndr, tcSubPat,
- badFieldCon, polyPatSig
- ) where
+module TcPat ( tcPat, tcPats, tcOverloadedLit,
+ PatCtxt(..), badFieldCon, polyPatSig ) where
#include "HsVersions.h"
-import HsSyn ( Pat(..), HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..) )
-import RnHsSyn ( RenamedPat )
-import TcHsSyn ( TcPat, TcId, hsLitType )
-
+import {-# SOURCE #-} TcExpr( tcSyntaxOp )
+import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
+ LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
+ collectPatsBinders, nlHsLit )
+import TcHsSyn ( TcId, hsLitType )
import TcRnMonad
-import Inst ( InstOrigin(..),
- newMethodFromName, newOverloadedLit, newDicts,
- instToId, tcInstDataCon, tcSyntaxName
+import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
+ newDicts, instToId, tcInstStupidTheta, isHsVar
)
-import Id ( mkLocalId, mkSysLocal )
-import Name ( Name )
-import FieldLabel ( fieldLabelName )
-import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupId )
-import TcMType ( newTyVarTy, zapToType, arityErr )
-import TcType ( TcType, TcTyVar, TcSigmaType,
- mkClassPred, liftedTypeKind )
-import TcUnify ( tcSubOff, TcHoleType,
- unifyTauTy, unifyListTy, unifyPArrTy, unifyTupleTy,
- mkCoercion, idCoercion, isIdCoercion,
- (<$>), PatCoFn )
-import TcMonoType ( tcHsSigType, UserTypeCtxt(..) )
-
-import TysWiredIn ( stringTy )
-import CmdLineOpts ( opt_IrrefutableTuples )
-import DataCon ( DataCon, dataConFieldLabels, dataConSourceArity )
-import PrelNames ( eqStringName, eqName, geName, negateName, minusName, cCallableClassName )
+import Id ( Id, idType, mkLocalId )
+import CoreFVs ( idFreeTyVars )
+import Name ( Name, mkSystemVarName )
+import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
+import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
+ tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
+ tcMetaTy )
+import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
+import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType,
+ SkolemInfo(PatSkol),
+ BoxySigmaType, BoxyRhoType,
+ pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar,
+ emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
+ mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy,
+ mkFunTy, mkFunTys, exactTyVarsOfTypes,
+ tidyOpenTypes )
+import VarSet ( elemVarSet, mkVarSet )
+import Kind ( liftedTypeKind, openTypeKind )
+import TcUnify ( boxySplitTyConApp, boxySplitListTy,
+ unBox, stripBoxyType, zapToMonotype,
+ boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
+import TcHsType ( UserTypeCtxt(..), tcPatSig )
+import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
+import Unify ( MaybeErr(..), gadtRefineTys )
+import Type ( substTys, substTheta )
+import StaticFlags ( opt_IrrefutableTuples )
+import TyCon ( TyCon )
+import DataCon ( DataCon, dataConTyCon, isVanillaDataCon,
+ dataConFieldLabels, dataConSourceArity, dataConSig )
+import PrelNames ( integralClassName, fromIntegerName, integerTyConName,
+ fromRationalName, rationalTyConName )
import BasicTypes ( isBoxed )
-import Bag
+import SrcLoc ( Located(..), SrcSpan, noLoc )
+import ErrUtils ( Message )
+import Util ( takeList, zipEqual )
import Outputable
import FastString
\end{code}
%************************************************************************
%* *
-\subsection{Variable patterns}
+ External interface
%* *
%************************************************************************
\begin{code}
-type BinderChecker = Name -> TcSigmaType -> TcM (PatCoFn, TcId)
- -- How to construct a suitable (monomorphic)
- -- Id for variables found in the pattern
- -- The TcSigmaType is the expected type
- -- from the pattern context
-
--- The Id may have a sigma type (e.g. f (x::forall a. a->a))
--- so we want to *create* it during pattern type checking.
--- We don't want to make Ids first with a type-variable type
--- and then unify... becuase we can't unify a sigma type with a type variable.
-
-tcMonoPatBndr :: BinderChecker
- -- This is the right function to pass to tcPat when
- -- we're looking at a lambda-bound pattern,
- -- so there's no polymorphic guy to worry about
-
-tcMonoPatBndr binder_name pat_ty
- = zapToType pat_ty `thenM` \ pat_ty' ->
- -- If there are *no constraints* on the pattern type, we
- -- revert to good old H-M typechecking, making
- -- the type of the binder into an *ordinary*
- -- type variable. We find out if there are no constraints
- -- by seeing if we are given an "open hole" as our info.
- -- What we are trying to avoid here is giving a binder
- -- a type that is a 'hole'. The only place holes should
- -- appear is as an argument to tcPat and tcExpr/tcMonoExpr.
-
- returnM (idCoercion, mkLocalId binder_name pat_ty')
+tcPats :: PatCtxt
+ -> [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,
+-- do the thing inside, use any existentially-bound dictionaries to
+-- discharge parts of the returning LIE, and deal with pattern type
+-- signatures
+
+-- 1. Initialise the PatState
+-- 2. Check the patterns
+-- 3. Apply the refinement
+-- 4. Check the body
+-- 5. Check that no existentials escape
+
+tcPats ctxt pats tys res_ty thing_inside
+ = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+
+ ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
+ refineEnvironment (pat_reft pstate') $
+ thing_inside (refineType (pat_reft pstate') res_ty)
+
+ ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+
+ ; returnM (pats', res) }
+
+
+-----------------
+tcPat :: PatCtxt
+ -> LPat Name -> BoxySigmaType
+ -> BoxyRhoType -- Result type
+ -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
+ -> TcM (LPat TcId, a)
+tcPat ctxt pat pat_ty res_ty thing_inside
+ = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
+ ; return (pat', thing) }
+
+
+-----------------
+tcCheckExistentialPat :: PatCtxt
+ -> [LPat TcId] -- Patterns (just for error message)
+ -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
+ -> [BoxySigmaType] -- Types of the patterns
+ -> BoxyRhoType -- Type of the body of the match
+ -- Tyvars in either of these must not escape
+ -> TcM ()
+-- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
+-- For example, we must reject this program:
+-- data C = forall a. C (a -> Int)
+-- f (C g) x = g x
+-- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
+
+tcCheckExistentialPat ctxt pats [] pat_tys body_ty
+ = return () -- Short cut for case when there are no existentials
+
+tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
+ -- Don't know how to deal with pattern-bound existentials yet
+ = failWithTc (existentialExplode pats)
+
+tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
+ = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys) $
+ checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
+
+data PatState = PS {
+ pat_ctxt :: PatCtxt,
+ pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
+ }
+
+data PatCtxt
+ = LamPat
+ | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
+
+patSigCtxt :: PatState -> UserTypeCtxt
+patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
+patSigCtxt other = LamPatSigCtxt
\end{code}
-%************************************************************************
-%* *
-\subsection{Typechecking patterns}
-%* *
-%************************************************************************
-
-\begin{code}
-tcPat :: BinderChecker
- -> RenamedPat
-
- -> TcHoleType -- Expected type derived from the context
- -- In the case of a function with a rank-2 signature,
- -- this type might be a forall type.
-
- -> TcM (TcPat,
- Bag TcTyVar, -- TyVars bound by the pattern
- -- These are just the existentially-bound ones.
- -- Any tyvars bound by *type signatures* in the
- -- patterns are brought into scope before we begin.
- Bag (Name, TcId), -- Ids bound by the pattern, along with the Name under
- -- which it occurs in the pattern
- -- The two aren't the same because we conjure up a new
- -- local name for each variable.
- [Inst]) -- Dicts or methods [see below] bound by the pattern
- -- from existential constructor patterns
-\end{code}
-
%************************************************************************
%* *
-\subsection{Variables, wildcards, lazy pats, as-pats}
+ Binders
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr pat@(TypePat ty) pat_ty
- = failWithTc (badTypePat pat)
-
-tcPat tc_bndr (VarPat name) pat_ty
- = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
- returnM (co_fn <$> VarPat bndr_id,
- emptyBag, unitBag (name, bndr_id), [])
-
-tcPat tc_bndr (LazyPat pat) pat_ty
- = tcPat tc_bndr pat pat_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
- returnM (LazyPat pat', tvs, ids, lie_avail)
-
-tcPat tc_bndr pat_in@(AsPat name pat) pat_ty
- = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
- tcPat tc_bndr pat pat_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
- returnM (co_fn <$> (AsPat bndr_id pat'),
- tvs, (name, bndr_id) `consBag` ids, lie_avail)
-
-tcPat tc_bndr (WildPat _) pat_ty
- = zapToType pat_ty `thenM` \ pat_ty' ->
- -- We might have an incoming 'hole' type variable; no annotation
- -- so zap it to a type. Rather like tcMonoPatBndr.
- returnM (WildPat pat_ty', emptyBag, emptyBag, [])
-
-tcPat tc_bndr (ParPat parend_pat) pat_ty
--- Leave the parens in, so that warnings from the
--- desugarer have parens in them
- = tcPat tc_bndr parend_pat pat_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
- returnM (ParPat pat', tvs, ids, lie_avail)
-
-tcPat tc_bndr pat_in@(SigPatIn pat sig) pat_ty
- = addErrCtxt (patCtxt pat_in) $
- tcHsSigType PatSigCtxt sig `thenM` \ sig_ty ->
- tcSubPat sig_ty pat_ty `thenM` \ co_fn ->
- tcPat tc_bndr pat sig_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
- returnM (co_fn <$> pat', tvs, ids, lie_avail)
+tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
+tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
+ = do { pat_ty' <- unBox pat_ty
+ -- We have an undecorated binder, so we do rule ABS1,
+ -- by unboxing the boxy type, forcing any un-filled-in
+ -- boxes to become monotypes
+ -- NB that pat_ty' can still be a polytype:
+ -- data T = MkT (forall a. a->a)
+ -- f t = case t of { MkT g -> ... }
+ -- Here, the 'g' must get type (forall a. a->a) from the
+ -- MkT context
+ ; return (mkLocalId bndr_name pat_ty') }
+
+tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
+ | Just mono_ty <- lookup_sig bndr_name
+ = do { mono_name <- newLocalName bndr_name
+ ; boxyUnify mono_ty pat_ty
+ ; return (mkLocalId mono_name mono_ty) }
+
+ | otherwise
+ = do { pat_ty' <- unBox pat_ty
+ ; mono_name <- newLocalName bndr_name
+ ; return (mkLocalId mono_name pat_ty') }
+
+
+-------------------
+bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
+bindInstsOfPatId id thing_inside
+ | not (isOverloadedTy (idType id))
+ = do { res <- thing_inside; return (res, emptyLHsBinds) }
+ | otherwise
+ = do { (res, lie) <- getLIE thing_inside
+ ; binds <- bindInstsOfLocalFuns lie [id]
+ ; return (res, binds) }
\end{code}
%************************************************************************
%* *
-\subsection{Explicit lists, parallel arrays, and tuples}
+ The main worker functions
%* *
%************************************************************************
-\begin{code}
-tcPat tc_bndr pat_in@(ListPat pats _) pat_ty
- = addErrCtxt (patCtxt pat_in) $
- unifyListTy pat_ty `thenM` \ elem_ty ->
- tcPats tc_bndr pats (repeat elem_ty) `thenM` \ (pats', tvs, ids, lie_avail) ->
- returnM (ListPat pats' elem_ty, tvs, ids, lie_avail)
-
-tcPat tc_bndr pat_in@(PArrPat pats _) pat_ty
- = addErrCtxt (patCtxt pat_in) $
- unifyPArrTy pat_ty `thenM` \ elem_ty ->
- tcPats tc_bndr pats (repeat elem_ty) `thenM` \ (pats', tvs, ids, lie_avail) ->
- returnM (PArrPat pats' elem_ty, tvs, ids, lie_avail)
+Note [Nesting]
+~~~~~~~~~~~~~~
+tcPat takes a "thing inside" over which the patter scopes. This is partly
+so that tcPat can extend the environment for the thing_inside, but also
+so that constraints arising in the thing_inside can be discharged by the
+pattern.
-tcPat tc_bndr pat_in@(TuplePat pats boxity) pat_ty
- = addErrCtxt (patCtxt pat_in) $
+This does not work so well for the ErrCtxt carried by the monad: we don't
+want the error-context for the pattern to scope over the RHS.
+Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
- unifyTupleTy boxity arity pat_ty `thenM` \ arg_tys ->
- tcPats tc_bndr pats arg_tys `thenM` \ (pats', tvs, ids, lie_avail) ->
+\begin{code}
+--------------------
+tc_lpats :: PatState
+ -> [LPat Name]
+ -> [BoxySigmaType]
+ -> (PatState -> TcM a)
+ -> TcM ([LPat TcId], [TcTyVar], a)
+
+tc_lpats pstate pats pat_tys thing_inside
+ = do { err_ctxt <- getErrCtxt
+ ; let loop pstate [] []
+ = do { res <- thing_inside pstate
+ ; return ([], [], res) }
+
+ loop pstate (p:ps) (ty:tys)
+ = do { (p', p_tvs, (ps', ps_tvs, res))
+ <- tc_lpat pstate p ty $ \ pstate' ->
+ setErrCtxt err_ctxt $
+ loop pstate' ps tys
+ -- setErrCtxt: restore context before doing the next pattern
+ -- See note [Nesting] above
+
+ ; return (p':ps', p_tvs ++ ps_tvs, res) }
+
+ loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
+
+ ; loop pstate pats pat_tys }
+
+--------------------
+tc_lpat :: PatState
+ -> LPat Name
+ -> BoxySigmaType
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat pstate (L span pat) pat_ty thing_inside
+ = setSrcSpan span $
+ maybeAddErrCtxt (patCtxt pat) $
+ do { let pat_ty' = refineType (pat_reft pstate) pat_ty
+ -- Make sure the result type reflects the current refinement
+ ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
+ ; return (L span pat', tvs, res) }
+
+
+--------------------
+tc_pat :: PatState
+ -> Pat Name -> BoxySigmaType -- Fully refined result type
+ -> (PatState -> TcM a) -- Thing inside
+ -> TcM (Pat TcId, -- Translated pattern
+ [TcTyVar], -- Existential binders
+ a) -- Result of thing inside
+
+tc_pat pstate (VarPat name) pat_ty thing_inside
+ = do { id <- tcPatBndr pstate name pat_ty
+ ; (res, binds) <- bindInstsOfPatId id $
+ tcExtendIdEnv1 name id $
+ (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
+ >> thing_inside pstate)
+ ; let pat' | isEmptyLHsBinds binds = VarPat id
+ | otherwise = VarPatOut id binds
+ ; return (pat', [], res) }
+
+tc_pat pstate (ParPat pat) pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; return (ParPat pat', tvs, res) }
+
+tc_pat pstate (BangPat pat) pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; return (BangPat pat', tvs, res) }
+
+-- There's a wrinkle with irrefuatable patterns, namely that we
+-- must not propagate type refinement from them. For example
+-- data T a where { T1 :: Int -> T Int; ... }
+-- f :: T a -> Int -> a
+-- f ~(T1 i) y = y
+-- It's obviously not sound to refine a to Int in the right
+-- hand side, because the arugment might not match T1 at all!
+--
+-- Nor should a lazy pattern bind any existential type variables
+-- because they won't be in scope when we do the desugaring
+tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
+ = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
+ thing_inside pstate
+ -- Ignore refined pstate',
+ -- revert to pstate
+ ; if (null pat_tvs) then return ()
+ else lazyPatErr lpat pat_tvs
+ ; return (LazyPat pat', [], res) }
+
+tc_pat pstate (WildPat _) pat_ty thing_inside
+ = do { pat_ty' <- unBox pat_ty -- Make sure it's filled in with monotypes
+ ; res <- thing_inside pstate
+ ; return (WildPat pat_ty', [], res) }
+
+tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
+ = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
+ ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
+ tc_lpat pstate pat (idType bndr_id) thing_inside
+ -- NB: if we do inference on:
+ -- \ (y@(x::forall a. a->a)) = e
+ -- we'll fail. The as-pattern infers a monotype for 'y', which then
+ -- fails to unify with the polymorphic type for 'x'. This could
+ -- perhaps be fixed, but only with a bit more work.
+ --
+ -- If you fix it, don't forget the bindInstsOfPatIds!
+ ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
+
+-- 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
+ ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
+ tc_lpat pstate pat inner_ty thing_inside
+ ; return (SigPatOut pat' inner_ty, tvs, res) }
+
+tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+ = failWithTc (badTypePat pat)
- -- possibly do the "make all tuple-pats irrefutable" test:
- let
- unmangled_result = TuplePat pats' boxity
+------------------------
+-- Lists, tuples, arrays
+tc_pat pstate (ListPat pats _) pat_ty thing_inside
+ = do { elt_ty <- boxySplitListTy pat_ty
+ ; let elt_tys = takeList pats (repeat elt_ty)
+ ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
+ ; return (ListPat pats' elt_ty, pats_tvs, res) }
+
+tc_pat pstate (PArrPat pats _) pat_ty thing_inside
+ = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
+ ; let elt_tys = takeList pats (repeat elt_ty)
+ ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
+ ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr
+ ; return (PArrPat pats' elt_ty, pats_tvs, res) }
+
+tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
+ = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
+ ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
-- so that we can experiment with lazy tuple-matching.
-- This is a pretty odd place to make the switch, but
-- it was easy to do.
-
- possibly_mangled_result
- | opt_IrrefutableTuples && isBoxed boxity = LazyPat unmangled_result
- | otherwise = unmangled_result
- in
- returnM (possibly_mangled_result, tvs, ids, lie_avail)
- where
- arity = length pats
+ ; let unmangled_result = TuplePat pats' boxity pat_ty
+ possibly_mangled_result
+ | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
+ | otherwise = unmangled_result
+
+ ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced
+ return (possibly_mangled_result, pats_tvs, res) }
+
+------------------------
+-- Data constructors
+tc_pat pstate pat_in@(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 }
+
+------------------------
+-- Literal patterns
+tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
+ = do { boxyUnify (hsLitType simple_lit) pat_ty
+ ; res <- thing_inside pstate
+ ; returnM (LitPat simple_lit, [], res) }
+
+------------------------
+-- Overloaded patterns: n, and n+k
+tc_pat pstate pat@(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)
+ ; mb_neg' <- case mb_neg of
+ Nothing -> return Nothing -- Positive literal
+ Just neg -> -- Negative literal
+ -- The 'negate' is re-mappable syntax
+ do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
+ ; return (Just neg') }
+ ; res <- thing_inside pstate
+ ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
+
+tc_pat pstate pat@(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
+ ; lit' <- tcOverloadedLit orig lit pat_ty'
+
+ -- The '>=' and '-' parts are re-mappable syntax
+ ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy)
+ ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
+
+ -- The Report says that n+k patterns must be in Integral
+ -- We may not want this when using re-mappable syntax, though (ToDo?)
+ ; icls <- tcLookupClass integralClassName
+ ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]
+ ; extendLIEs dicts
+
+ ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
+ ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
\end{code}
%************************************************************************
%* *
-\subsection{Other constructors}
+ Most of the work for constructors is here
+ (the rest is in the ConPatIn case of tc_pat)
%* *
-
%************************************************************************
\begin{code}
-tcPat tc_bndr pat_in@(ConPatIn con_name arg_pats) pat_ty
- = addErrCtxt (patCtxt pat_in) $
+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)
+ } }
+ where
+ doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
+
+tcConArgs :: PatState -> DataCon
+ -> HsConDetails Name (LPat Name) -> [TcSigmaType]
+ -> (PatState -> TcM a)
+ -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
+
+tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
+ = do { checkTc (con_arity == no_of_args) -- Check correct arity
+ (arityErr "Constructor" data_con con_arity no_of_args)
+ ; (arg_pats', tvs, res) <- tc_lpats pstate arg_pats arg_tys thing_inside
+ ; return (PrefixCon arg_pats', tvs, res) }
+ where
+ con_arity = dataConSourceArity data_con
+ no_of_args = length arg_pats
- -- Check that it's a constructor, and instantiate it
- tcLookupDataCon con_name `thenM` \ data_con ->
- tcInstDataCon (PatOrigin pat_in) data_con `thenM` \ (_, ex_dicts1, arg_tys, con_res_ty, ex_tvs) ->
+tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
+ = do { checkTc (con_arity == 2) -- Check correct arity
+ (arityErr "Constructor" data_con con_arity 2)
+ ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
+ ; return (InfixCon p1' p2', tvs, res) }
+ where
+ con_arity = dataConSourceArity data_con
- -- Check overall type matches.
- -- The pat_ty might be a for-all type, in which
- -- case we must instantiate to match
- tcSubPat con_res_ty pat_ty `thenM` \ co_fn ->
+tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
+ = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
+ ; return (RecCon rpats', tvs, res) }
+ where
+ tc_fields :: PatState -> [(Located Name, LPat Name)]
+ -> (PatState -> TcM a)
+ -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
+ tc_fields pstate [] thing_inside
+ = do { res <- thing_inside pstate
+ ; return ([], [], res) }
+
+ tc_fields pstate (rpat : rpats) thing_inside
+ = do { (rpat', tvs1, (rpats', tvs2, res))
+ <- tc_field pstate rpat $ \ pstate' ->
+ tc_fields pstate' rpats thing_inside
+ ; return (rpat':rpats', tvs1 ++ tvs2, res) }
+
+ tc_field pstate (field_lbl, pat) thing_inside
+ = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
+ ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; return ((sel_id, pat'), tvs, res) }
+
+ find_field_ty field_lbl
+ = case [ty | (f,ty) <- field_tys, f == field_lbl] of
- -- Check the argument patterns
- tcConStuff tc_bndr data_con arg_pats arg_tys `thenM` \ (arg_pats', arg_tvs, arg_ids, ex_dicts2) ->
+ -- No matching field; chances are this field label comes from some
+ -- other record type (or maybe none). As well as reporting an
+ -- error we still want to typecheck the pattern, principally to
+ -- make sure that all the variables it binds are put into the
+ -- environment, else the type checker crashes later:
+ -- f (R { foo = (a,b) }) = a+b
+ -- If foo isn't one of R's fields, we don't want to crash when
+ -- typechecking the "a+b".
+ [] -> do { addErrTc (badFieldCon data_con field_lbl)
+ ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
+ ; return (error "Bogus selector Id", bogus_ty) }
- returnM (co_fn <$> ConPatOut data_con arg_pats' con_res_ty ex_tvs (map instToId ex_dicts1),
- listToBag ex_tvs `unionBags` arg_tvs,
- arg_ids,
- ex_dicts1 ++ ex_dicts2)
+ -- The normal case, when the field comes from the right constructor
+ (pat_ty : extras) ->
+ ASSERT( null extras )
+ do { sel_id <- tcLookupId field_lbl
+ ; return (sel_id, pat_ty) }
+
+ field_tys = zip (dataConFieldLabels data_con) arg_tys
+ -- Don't use zipEqual! If the constructor isn't really a record, then
+ -- dataConFieldLabels will be empty (and each field in the pattern
+ -- will generate an error below).
\end{code}
%************************************************************************
%* *
-\subsection{Literals}
+ Type refinement
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr (LitPat lit@(HsLitLit s _)) pat_ty
- -- cf tcExpr on LitLits
- = tcLookupClass cCallableClassName `thenM` \ cCallableClass ->
- newDicts (LitLitOrigin (unpackFS s))
- [mkClassPred cCallableClass [pat_ty]] `thenM` \ dicts ->
- extendLIEs dicts `thenM_`
- returnM (LitPat (HsLitLit s pat_ty), emptyBag, emptyBag, [])
-
-tcPat tc_bndr pat@(LitPat lit@(HsString _)) pat_ty
- = unifyTauTy pat_ty stringTy `thenM_`
- tcLookupId eqStringName `thenM` \ eq_id ->
- returnM (NPatOut lit stringTy (HsVar eq_id `HsApp` HsLit lit),
- emptyBag, emptyBag, [])
-
-tcPat tc_bndr (LitPat simple_lit) pat_ty
- = unifyTauTy pat_ty (hsLitType simple_lit) `thenM_`
- returnM (LitPat simple_lit, emptyBag, emptyBag, [])
-
-tcPat tc_bndr pat@(NPatIn over_lit mb_neg) pat_ty
- = newOverloadedLit origin over_lit pat_ty `thenM` \ pos_lit_expr ->
- newMethodFromName origin pat_ty eqName `thenM` \ eq ->
- (case mb_neg of
- Nothing -> returnM pos_lit_expr -- Positive literal
- Just neg -> -- Negative literal
- -- The 'negate' is re-mappable syntax
- tcSyntaxName origin pat_ty negateName neg `thenM` \ (neg_expr, _) ->
- returnM (HsApp neg_expr pos_lit_expr)
- ) `thenM` \ lit_expr ->
-
- returnM (NPatOut lit' pat_ty (HsApp (HsVar eq) lit_expr),
- emptyBag, emptyBag, [])
- where
- origin = PatOrigin pat
-
- -- The literal in an NPatIn is always positive...
- -- But in NPat, the literal is used to find identical patterns
- -- so we must negate the literal when necessary!
- lit' = case (over_lit, mb_neg) of
- (HsIntegral i _, Nothing) -> HsInteger i
- (HsIntegral i _, Just _) -> HsInteger (-i)
- (HsFractional f _, Nothing) -> HsRat f pat_ty
- (HsFractional f _, Just _) -> HsRat (-f) pat_ty
+refineAlt :: PatState
+ -> DataCon -- For tracing only
+ -> [TcTyVar] -- Type variables from pattern
+ -> [Bool] -- Flags indicating which type variables occur
+ -- in the type of at least one argument
+ -> [TcType] -- Result types from the pattern
+ -> [BoxySigmaType] -- Result types from the scrutinee (context)
+ -> (PatState -> [BoxySigmaType] -> TcM a)
+ -- Possibly-refined existentials
+ -> TcM a
+refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
+ | not (all isRigidTy ctxt_res_tys)
+ -- The context is not a rigid type, so we do no type refinement here.
+ = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
+ subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
+
+ res_tvs = tcTyVarsOfTypes pat_res_tys
+ -- The tvs are (already) all fresh skolems. We need a
+ -- fresh skolem for each type variable (to bind in the pattern)
+ -- even if it's refined away by the type refinement
+ find_inst tv
+ | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv)
+ | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
+ | otherwise = do { tv <- newBoxyTyVar openTypeKind
+ ; return (mkTyVarTy tv) }
+ ; pat_tys' <- mapM find_inst pat_tvs
+
+ -- Do the thing inside
+ ; res <- thing_inside pstate pat_tys'
+
+ -- Unbox the types that have been filled in by the thing_inside
+ -- I.e. the ones whose type variables are mentioned in at least one arg
+ ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
+ | otherwise = return ty
+ ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
+ ; let subst = zipOpenTvSubst pat_tvs pat_tys''
+ ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
+
+ ; return res } -- All boxes now filled
+
+ | otherwise -- The context is rigid, so we can do type refinement
+ = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
+ Failed msg -> failWithTc (inaccessibleAlt msg)
+ Succeeded (new_subst, all_bound_here)
+ | all_bound_here -- All the new bindings are for pat_tvs, so no need
+ -- to refine the environment or pstate
+ -> do { traceTc trace_msg
+ ; thing_inside pstate pat_tvs' }
+ | otherwise -- New bindings affect the context, so pass down pstate'.
+ -- DO NOT refine the envt, because we might be inside a
+ -- lazy pattern
+ -> do { traceTc trace_msg
+ ; thing_inside pstate' pat_tvs' }
+ where
+ pat_tvs' = map (substTyVar new_subst) pat_tvs
+ pstate' = pstate { pat_reft = new_subst }
+ trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
+
+refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
+-- Refine the type if it is rigid
+refineType reft ty
+ | isRefineableTy ty = substTy reft ty
+ | otherwise = ty
\end{code}
-%************************************************************************
-%* *
-\subsection{n+k patterns}
-%* *
-%************************************************************************
-
-\begin{code}
-tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsIntegral i _) minus_name) pat_ty
- = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
- newOverloadedLit origin lit pat_ty `thenM` \ over_lit_expr ->
- newMethodFromName origin pat_ty geName `thenM` \ ge ->
-
- -- The '-' part is re-mappable syntax
- tcSyntaxName origin pat_ty minusName minus_name `thenM` \ (minus_expr, _) ->
-
- returnM (NPlusKPatOut bndr_id i
- (SectionR (HsVar ge) over_lit_expr)
- (SectionR minus_expr over_lit_expr),
- emptyBag, unitBag (name, bndr_id), [])
- where
- origin = PatOrigin pat
-\end{code}
%************************************************************************
%* *
-\subsection{Lists of patterns}
+ Overloaded literals
%* *
%************************************************************************
-Helper functions
+In tcOverloadedLit we convert directly to an Int or Integer if we
+know that's what we want. This may save some time, by not
+temporarily generating overloaded literals, but it won't catch all
+cases (the rest are caught in lookupInst).
\begin{code}
-tcPats :: BinderChecker -- How to deal with variables
- -> [RenamedPat] -> [TcType] -- Excess 'expected types' discarded
- -> TcM ([TcPat],
- Bag TcTyVar,
- Bag (Name, TcId), -- Ids bound by the pattern
- [Inst]) -- Dicts bound by the pattern
-
-tcPats tc_bndr [] tys = returnM ([], emptyBag, emptyBag, [])
-
-tcPats tc_bndr (ty:tys) (pat:pats)
- = tcPat tc_bndr ty pat `thenM` \ (pat', tvs1, ids1, lie_avail1) ->
- tcPats tc_bndr tys pats `thenM` \ (pats', tvs2, ids2, lie_avail2) ->
-
- returnM (pat':pats',
- tvs1 `unionBags` tvs2, ids1 `unionBags` ids2,
- lie_avail1 ++ lie_avail2)
+tcOverloadedLit :: InstOrigin
+ -> HsOverLit Name
+ -> BoxyRhoType
+ -> TcM (HsOverLit TcId)
+tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
+ | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
+ -- Reason: If we do, tcSimplify will call lookupInst, which
+ -- will call tcSyntaxName, which does unification,
+ -- which tcSimplify doesn't like
+ -- ToDo: noLoc sadness
+ = do { integer_ty <- tcMetaTy integerTyConName
+ ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
+ ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
+
+ | Just expr <- shortCutIntLit i res_ty
+ = return (HsIntegral i expr)
+
+ | otherwise
+ = do { expr <- newLitInst orig lit res_ty
+ ; return (HsIntegral i expr) }
+
+tcOverloadedLit orig lit@(HsFractional r fr) res_ty
+ | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
+ = do { rat_ty <- tcMetaTy rationalTyConName
+ ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
+ -- Overloaded literals must have liftedTypeKind, because
+ -- we're instantiating an overloaded function here,
+ -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
+ -- However this'll be picked up by tcSyntaxOp if necessary
+ ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
+
+ | Just expr <- shortCutFracLit r res_ty
+ = return (HsFractional r expr)
+
+ | otherwise
+ = do { expr <- newLitInst orig lit res_ty
+ ; return (HsFractional r expr) }
+
+newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
+newLitInst orig lit res_ty -- Make a LitInst
+ = do { loc <- getInstLoc orig
+ ; res_tau <- zapToMonotype res_ty
+ ; new_uniq <- newUnique
+ ; let
+ lit_nm = mkSystemVarName new_uniq FSLIT("lit")
+ lit_inst = LitInst lit_nm lit res_tau loc
+ ; extendLIE lit_inst
+ ; return (HsVar (instToId lit_inst)) }
\end{code}
%************************************************************************
%* *
-\subsection{Constructor arguments}
+ Note [Pattern coercions]
%* *
%************************************************************************
-\begin{code}
-tcConStuff tc_bndr data_con (PrefixCon arg_pats) arg_tys
- = -- Check correct arity
- checkTc (con_arity == no_of_args)
- (arityErr "Constructor" data_con con_arity no_of_args) `thenM_`
-
- -- Check arguments
- tcPats tc_bndr arg_pats arg_tys `thenM` \ (arg_pats', tvs, ids, lie_avail) ->
+In principle, these program would be reasonable:
+
+ f :: (forall a. a->a) -> Int
+ f (x :: Int->Int) = x 3
- returnM (PrefixCon arg_pats', tvs, ids, lie_avail)
- where
- con_arity = dataConSourceArity data_con
- no_of_args = length arg_pats
+ g :: (forall a. [a]) -> Bool
+ g [] = True
-tcConStuff tc_bndr data_con (InfixCon p1 p2) arg_tys
- = -- Check correct arity
- checkTc (con_arity == 2)
- (arityErr "Constructor" data_con con_arity 2) `thenM_`
+In both cases, the function type signature restricts what arguments can be passed
+in a call (to polymorphic ones). The pattern type signature then instantiates this
+type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
+generate the translated term
+ f = \x' :: (forall a. a->a). let x = x' Int in x 3
- -- Check arguments
- tcPat tc_bndr p1 ty1 `thenM` \ (p1', tvs1, ids1, lie_avail1) ->
- tcPat tc_bndr p2 ty2 `thenM` \ (p2', tvs2, ids2, lie_avail2) ->
-
- returnM (InfixCon p1' p2',
- tvs1 `unionBags` tvs2, ids1 `unionBags` ids2,
- lie_avail1 ++ lie_avail2)
- where
- con_arity = dataConSourceArity data_con
- [ty1, ty2] = arg_tys
+From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
+And it requires a significant amount of code to implement, becuase we need to decorate
+the translated pattern with coercion functions (generated from the subsumption check
+by tcSub).
-tcConStuff tc_bndr data_con (RecCon rpats) arg_tys
- = -- Check the fields
- tc_fields field_tys rpats `thenM` \ (rpats', tvs, ids, lie_avail) ->
- returnM (RecCon rpats', tvs, ids, lie_avail)
-
- where
- field_tys = zip (map fieldLabelName (dataConFieldLabels data_con)) arg_tys
- -- Don't use zipEqual! If the constructor isn't really a record, then
- -- dataConFieldLabels will be empty (and each field in the pattern
- -- will generate an error below).
-
- tc_fields field_tys []
- = returnM ([], emptyBag, emptyBag, [])
-
- tc_fields field_tys ((field_label, rhs_pat) : rpats)
- = tc_fields field_tys rpats `thenM` \ (rpats', tvs1, ids1, lie_avail1) ->
-
- (case [ty | (f,ty) <- field_tys, f == field_label] of
-
- -- No matching field; chances are this field label comes from some
- -- other record type (or maybe none). As well as reporting an
- -- error we still want to typecheck the pattern, principally to
- -- make sure that all the variables it binds are put into the
- -- environment, else the type checker crashes later:
- -- f (R { foo = (a,b) }) = a+b
- -- If foo isn't one of R's fields, we don't want to crash when
- -- typechecking the "a+b".
- [] -> addErrTc (badFieldCon data_con field_label) `thenM_`
- newTyVarTy liftedTypeKind `thenM` \ bogus_ty ->
- returnM (error "Bogus selector Id", bogus_ty)
+So for now I'm just insisting on type *equality* in patterns. No subsumption.
- -- The normal case, when the field comes from the right constructor
- (pat_ty : extras) ->
- ASSERT( null extras )
- tcLookupId field_label `thenM` \ sel_id ->
- returnM (sel_id, pat_ty)
- ) `thenM` \ (sel_id, pat_ty) ->
+Old notes about desugaring, at a time when pattern coercions were handled:
- tcPat tc_bndr rhs_pat pat_ty `thenM` \ (rhs_pat', tvs2, ids2, lie_avail2) ->
+A SigPat is a type coercion and must be handled one at at time. We can't
+combine them unless the type of the pattern inside is identical, and we don't
+bother to check for that. For example:
- returnM ((sel_id, rhs_pat') : rpats',
- tvs1 `unionBags` tvs2,
- ids1 `unionBags` ids2,
- lie_avail1 ++ lie_avail2)
-\end{code}
+ data T = T1 Int | T2 Bool
+ f :: (forall a. a -> a) -> T -> t
+ f (g::Int->Int) (T1 i) = T1 (g i)
+ f (g::Bool->Bool) (T2 b) = T2 (g b)
+We desugar this as follows:
-%************************************************************************
-%* *
-\subsection{Subsumption}
-%* *
-%************************************************************************
+ f = \ g::(forall a. a->a) t::T ->
+ let gi = g Int
+ in case t of { T1 i -> T1 (gi i)
+ other ->
+ let gb = g Bool
+ in case t of { T2 b -> T2 (gb b)
+ other -> fail }}
-Example:
- f :: (forall a. a->a) -> Int -> Int
- f (g::Int->Int) y = g y
-This is ok: the type signature allows fewer callers than
-the (more general) signature f :: (Int->Int) -> Int -> Int
-I.e. (forall a. a->a) <= Int -> Int
-We end up translating this to:
- f = \g' :: (forall a. a->a). let g = g' Int in g' y
-
-tcSubPat does the work
- sig_ty is the signature on the pattern itself
- (Int->Int in the example)
- expected_ty is the type passed inwards from the context
- (forall a. a->a in the example)
+Note that we do not treat the first column of patterns as a
+column of variables, because the coerced variables (gi, gb)
+would be of different types. So we get rather grotty code.
+But I don't think this is a common case, and if it was we could
+doubtless improve it.
-\begin{code}
-tcSubPat :: TcSigmaType -> TcHoleType -> TcM PatCoFn
-
-tcSubPat sig_ty exp_ty
- = tcSubOff sig_ty exp_ty `thenM` \ co_fn ->
- -- co_fn is a coercion on *expressions*, and we
- -- need to make a coercion on *patterns*
- if isIdCoercion co_fn then
- returnM idCoercion
- else
- newUnique `thenM` \ uniq ->
- let
- arg_id = mkSysLocal FSLIT("sub") uniq exp_ty
- the_fn = DictLam [arg_id] (co_fn <$> HsVar arg_id)
- pat_co_fn p = SigPatOut p exp_ty the_fn
- in
- returnM (mkCoercion pat_co_fn)
-\end{code}
+Meanwhile, the strategy is:
+ * treat each SigPat coercion (always non-identity coercions)
+ as a separate block
+ * deal with the stuff inside, and then wrap a binding round
+ the result to bind the new variable (gi, gb, etc)
%************************************************************************
%************************************************************************
\begin{code}
-patCtxt pat = hang (ptext SLIT("When checking the pattern:"))
- 4 (ppr pat)
+patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context
+patCtxt (VarPat _) = Nothing
+patCtxt (ParPat _) = Nothing
+patCtxt (AsPat _ _) = Nothing
+patCtxt pat = Just (hang (ptext SLIT("In the pattern:"))
+ 4 (ppr pat))
+
+-----------------------------------------------
+
+existentialExplode pats
+ = 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 (vcat (map ppr pats))
+
+sigPatCtxt bound_ids bound_tvs tys tidy_env
+ = -- tys is (body_ty : pat_tys)
+ mapM zonkTcType tys `thenM` \ tys' ->
+ let
+ (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
+ (_env2, tidy_body_ty : tidy_pat_tys) = tidyOpenTypes env1 tys'
+ in
+ returnM (env1,
+ sep [ptext SLIT("When checking an existential match that binds"),
+ nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
+ ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
+ ptext SLIT("The body has type:") <+> ppr tidy_body_ty
+ ])
+ where
+ show_ids = filter is_interesting bound_ids
+ is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
+
+ ppr_id id ty = ppr id <+> dcolon <+> ppr ty
+ -- Don't zonk the types so we get the separate, un-unified versions
badFieldCon :: DataCon -> Name -> SDoc
badFieldCon con field
4 (ppr sig_ty)
badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
-\end{code}
+lazyPatErr pat tvs
+ = failWithTc $
+ hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
+ 2 (vcat (map pprSkolTvBinding tvs))
+
+inaccessibleAlt msg
+ = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
+\end{code}