representation and family type. It is accessible from :R123Map via
tyConFamilyCoercion_maybe and has kind
- Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+ Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
The wrapper and worker of MapPair get the types
id_arg1 = mkTemplateLocal 1
(if null orig_arg_tys
- then ASSERT(not (null $ dataConDictTheta data_con)) mkPredTy $ head (dataConDictTheta data_con)
+ then ASSERT(not (null $ dataConDictTheta data_con))
+ mkPredTy $ head (dataConDictTheta data_con)
else head orig_arg_tys
)
-- ...(let w = C x in ...(w p q)...)...
-- we want to see that w is strict in its two arguments
- wrap_unf = mkTopUnfolding $ Note InlineMe $
- mkLams wrap_tvs $
- mkLams eq_args $
- mkLams dict_args $ mkLams id_args $
- foldr mk_case con_app
- (zip (dict_args ++ id_args) all_strict_marks)
- i3 []
+ wrap_unf = mkImplicitUnfolding $ Note InlineMe $
+ mkLams wrap_tvs $
+ mkLams eq_args $
+ mkLams dict_args $ mkLams id_args $
+ foldr mk_case con_app
+ (zip (dict_args ++ id_args) all_strict_marks)
+ i3 []
con_app _ rep_ids = wrapFamInstBody tycon res_ty_args $
Var wrk_id `mkTyApps` res_ty_args
result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
E.g.
data T where
- T1 { f :: a } :: T [a]
- T2 { f :: a, y :: b } :: T [a]
-and now the selector takes that type as its argument:
- f :: forall a. T [a] -> a
- f t = case t of
- T1 { f = v } -> v
- T2 { f = v } -> v
+ T1 { f :: Maybe a } :: T [a]
+ T2 { f :: Maybe a, y :: b } :: T [a]
+
+and now the selector takes that result type as its argument:
+ f :: forall a. T [a] -> Maybe a
+
+Details: the "real" types of T1,T2 are:
+ T1 :: forall r a. (r~[a]) => a -> T r
+ T2 :: forall r a b. (r~[a]) => a -> b -> T r
+
+So the selector loooks like this:
+ f :: forall a. T [a] -> Maybe a
+ f (a:*) (t:T [a])
+ = case t of
+ T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
+ T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
+
Note the forall'd tyvars of the selector are just the free tyvars
of the result type; there may be other tyvars in the constructor's
type (e.g. 'b' in T2).
+Note the need for casts in the result!
+
Note [Selector running example]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's OK to combine GADTs and type families. Here's a running example:
info = noCafIdInfo
`setCafInfo` caf_info
`setArityInfo` arity
- `setUnfoldingInfo` mkTopUnfolding rhs_w_str
+ `setUnfoldingInfo` unfolding
`setAllStrictnessInfo` Just strict_sig
+ unfolding = mkImplicitUnfolding rhs_w_str
+
-- Allocate Ids. We do it a funny way round because field_dict_tys is
-- almost always empty. Also note that we use max_dict_tys
-- rather than n_dict_tys, because the latter gives an infinite loop:
-- foo = /\a. \t:T. case t of { MkT f -> f a }
mk_alt data_con
- = ASSERT2( data_ty `tcEqType` field_ty,
- ppr data_con $$ ppr data_ty $$ ppr field_ty )
- mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
+ = mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
where
-- get pattern binders with types appropriately instantiated
arg_uniqs = map mkBuiltinUnique [arg_base..]
rebox_uniqs = map mkBuiltinUnique [rebox_base..]
-- data T :: *->* where T1 { fld :: Maybe b } -> T [b]
- -- Hence T1 :: forall a b. (a=[b]) => b -> T a
+ -- Hence T1 :: forall a b. (a~[b]) => b -> T a
-- fld :: forall b. T [b] -> Maybe b
-- fld = /\b.\(t:T[b]). case t of
-- T1 b' (c : [b]=[b']) (x:Maybe b')
-- -> x `cast` Maybe (sym (right c))
- -- Generate the refinement for b'=b,
- -- and apply to (Maybe b'), to get (Maybe b)
- reft = matchRefine co_tvs
- the_arg_id_ty = idType the_arg_id
- (rhs, data_ty) =
- case refineType reft the_arg_id_ty of
- Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty)
- Nothing -> (Var the_arg_id, the_arg_id_ty)
+ -- Generate the cast for the result
+ -- See Note [GADT record selectors] for why a cast is needed
+ in_scope_tvs = ex_tvs ++ co_tvs ++ data_tvs
+ reft = matchRefine in_scope_tvs (map (mkSymCoercion . mkTyVarTy) co_tvs)
+ rhs = case refineType reft (idType the_arg_id) of
+ Nothing -> Var the_arg_id
+ Just (co, data_ty) -> ASSERT2( data_ty `tcEqType` field_ty,
+ ppr data_con $$ ppr data_ty $$ ppr field_ty )
+ Cast (Var the_arg_id) co
field_vs = filter (not . isPredTy . idType) arg_vs
the_arg_id = assoc "mkRecordSelId:mk_alt"
`setArityInfo` 1
`setAllStrictnessInfo` Just strict_sig
`setUnfoldingInfo` (if no_unf then noUnfolding
- else mkTopUnfolding rhs)
+ else mkImplicitUnfolding rhs)
-- We no longer use 'must-inline' on record selectors. They'll
-- inline like crazy if they scrutinise a constructor
lazyIdName = mkWiredInIdName gHC_BASE (fsLit "lazy") lazyIdKey lazyId
errorName = mkWiredInIdName gHC_ERR (fsLit "error") errorIdKey eRROR_ID
-recSelErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "recSelError") recSelErrorIdKey rEC_SEL_ERROR_ID
-runtimeErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "runtimeError") runtimeErrorIdKey rUNTIME_ERROR_ID
-irrefutPatErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "irrefutPatError") irrefutPatErrorIdKey iRREFUT_PAT_ERROR_ID
-recConErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "recConError") recConErrorIdKey rEC_CON_ERROR_ID
-patErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "patError") patErrorIdKey pAT_ERROR_ID
-noMethodBindingErrorName = mkWiredInIdName cONTROL_EXCEPTION (fsLit "noMethodBindingError")
+recSelErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "recSelError") recSelErrorIdKey rEC_SEL_ERROR_ID
+runtimeErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "runtimeError") runtimeErrorIdKey rUNTIME_ERROR_ID
+irrefutPatErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "irrefutPatError") irrefutPatErrorIdKey iRREFUT_PAT_ERROR_ID
+recConErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "recConError") recConErrorIdKey rEC_CON_ERROR_ID
+patErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "patError") patErrorIdKey pAT_ERROR_ID
+noMethodBindingErrorName = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "noMethodBindingError")
noMethodBindingErrorIdKey nO_METHOD_BINDING_ERROR_ID
nonExhaustiveGuardsErrorName
- = mkWiredInIdName gHC_ERR (fsLit "nonExhaustiveGuardsError")
+ = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit "nonExhaustiveGuardsError")
nonExhaustiveGuardsErrorIdKey nON_EXHAUSTIVE_GUARDS_ERROR_ID
\end{code}
projects / ghc-hetmet.git / blobdiff