#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcSyntaxOp )
-import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
+import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..),
+ HsOverLit(..), HsExpr(..), OutPat, ExprCoFn(..),
mkCoPat, idCoercion,
LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
collectPatsBinders, nlHsLit )
tcLookupClass, tcLookupDataCon, refineEnvironment,
tcLookupField, tcMetaTy )
import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars,
-+ newCoVars, zonkTcType )
+ newCoVars, zonkTcType, tcInstTyVars )
import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
SkolemInfo(PatSkol),
BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
import {- Kind parts of -}
Type ( liftedTypeKind )
import TcUnify ( boxySplitTyConApp, boxySplitListTy, unBox,
- zapToMonotype, boxyUnify, checkSigTyVarsWrt,
- unifyType )
+ zapToMonotype, boxyUnify, boxyUnifyList,
+ checkSigTyVarsWrt, unifyType )
import TcHsType ( UserTypeCtxt(..), tcPatSig )
import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
-import Type ( substTys, substTheta )
+import Type ( Type, mkTyConApp, substTys, substTheta )
import StaticFlags ( opt_IrrefutableTuples )
-import TyCon ( TyCon, FieldLabel )
+import TyCon ( TyCon, FieldLabel, tyConFamInst_maybe,
+ tyConFamilyCoercion_maybe, tyConTyVars )
import DataCon ( DataCon, dataConTyCon, dataConFullSig, dataConName,
dataConFieldLabels, dataConSourceArity,
dataConStupidTheta, dataConUnivTyVars )
%* *
%************************************************************************
+[Pattern matching indexed data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following declarations:
+
+ data family Map k :: * -> *
+ data instance Map (a, b) v = MapPair (Map a (Pair b v))
+
+and a case expression
+
+ case x :: Map (Int, c) w of MapPair m -> ...
+
+As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
+worker/wrapper types for MapPair are
+
+ $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+ $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
+:R123Map, which means the straight use of boxySplitTyConApp would give a type
+error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
+boxySplitTyConApp with the family tycon Map instead, which gives us the family
+type list {(Int, c), w}. To get the correct split for :R123Map, we need to
+unify the family type list {(Int, c), w} with the instance types {(a, b), v}
+(provided by tyConFamInst_maybe together with the family tycon). This
+unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
+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}
+
+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
+from the family to the representation type. This is achieved by
+unwrapFamInstScrutinee using a CoPat around the result pattern.
+
+Now it might appear seem as if we could have used the existing GADT type
+refinement infrastructure of refineAlt and friends instead of the explicit
+unification and CoPat generation. However, that would be wrong. Why? The
+whole point of GADT refinement is that the refinement is local to the case
+alternative. In contrast, the substitution generated by the unification of
+the family type list and instance types needs to be propagated to the outside.
+Imagine that in the above example, the type of the scrutinee would have been
+(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
+substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
+instantiation of x with (a, b) must be global; ie, it must be valid in *all*
+alternatives of the case expression, whereas in the GADT case it might vary
+between alternatives.
+
+In fact, if we have a data instance declaration defining a GADT, eq_spec will
+be non-empty and we will get a mixture of global instantiations and local
+refinement from a single match. This neatly reflects that, as soon as we
+have constrained the type of the scrutinee to the required type index, all
+further type refinement is local to the alternative.
+
\begin{code}
-- Running example:
-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
origin = SigOrigin skol_info
-- Instantiate the constructor type variables [a->ty]
- ; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty
+ ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
(ctxt_res_tys ++ mkTyVarTys ex_tvs')
; addDataConStupidTheta origin data_con ctxt_res_tys
- ; return (ConPatOut { pat_con = L con_span data_con,
- pat_tvs = ex_tvs' ++ co_vars,
- pat_dicts = map instToId dicts, pat_binds = dict_binds,
- pat_args = arg_pats', pat_ty = pat_ty },
- ex_tvs' ++ inner_tvs, res)
+ ; return
+ (unwrapFamInstScrutinee tycon ctxt_res_tys $
+ ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = ex_tvs' ++ co_vars,
+ pat_dicts = map instToId dicts,
+ pat_binds = dict_binds,
+ pat_args = arg_pats', pat_ty = pat_ty },
+ ex_tvs' ++ inner_tvs, res)
}
where
doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
+ -- Split against the family tycon if the pattern constructor belongs to a
+ -- representation tycon.
+ --
+ boxySplitTyConAppWithFamily tycon pat_ty =
+ case tyConFamInst_maybe tycon of
+ Nothing -> boxySplitTyConApp tycon pat_ty
+ Just (fam_tycon, instTys) ->
+ do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
+ ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
+ ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
+ ; return freshTvs
+ }
+
+ -- 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
+ | Just co_con <- tyConFamilyCoercion_maybe tycon
+ -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
+ -- coercion is not the identity; mkCoPat is inconvenient as it
+ -- wants a located pattern.
+ = CoPat (ExprCoFn $ mkTyConApp co_con args) -- co fam ty to repr ty
+ (pat {pat_ty = mkTyConApp tycon args}) -- representation type
+ pat_ty -- family inst type
+ | otherwise
+ = pat
+
+
tcConArgs :: DataCon -> [TcSigmaType]
- -> Checker (HsConDetails Name (LPat Name)) (HsConDetails Id (LPat Id))
+ -> Checker (HsConDetails Name (LPat Name))
+ (HsConDetails Id (LPat Id))
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
= do { checkTc (con_arity == no_of_args) -- Check correct arity
projects / ghc-hetmet.git / blobdiff