Add kind equalities to GHC.
[ghc.git] / compiler / iface / BuildTyCl.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 -}
5
6 {-# LANGUAGE CPP #-}
7
8 module BuildTyCl (
9 buildDataCon,
10 buildPatSyn,
11 TcMethInfo, buildClass,
12 distinctAbstractTyConRhs, totallyAbstractTyConRhs,
13 mkNewTyConRhs, mkDataTyConRhs,
14 newImplicitBinder, newTyConRepName
15 ) where
16
17 #include "HsVersions.h"
18
19 import IfaceEnv
20 import FamInstEnv( FamInstEnvs )
21 import TysWiredIn( isCTupleTyConName )
22 import PrelNames( tyConRepModOcc )
23 import DataCon
24 import PatSyn
25 import Var
26 import VarSet
27 import BasicTypes
28 import Name
29 import MkId
30 import Class
31 import TyCon
32 import Type
33 import Id
34 import Coercion
35 import TcType
36
37 import SrcLoc( noSrcSpan )
38 import DynFlags
39 import TcRnMonad
40 import UniqSupply
41 import Util
42 import Outputable
43
44 distinctAbstractTyConRhs, totallyAbstractTyConRhs :: AlgTyConRhs
45 distinctAbstractTyConRhs = AbstractTyCon True
46 totallyAbstractTyConRhs = AbstractTyCon False
47
48 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
49 mkDataTyConRhs cons
50 = DataTyCon {
51 data_cons = cons,
52 is_enum = not (null cons) && all is_enum_con cons
53 -- See Note [Enumeration types] in TyCon
54 }
55 where
56 is_enum_con con
57 | (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res)
58 <- dataConFullSig con
59 = null ex_tvs && null eq_spec && null theta && null arg_tys
60
61
62 mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
63 -- ^ Monadic because it makes a Name for the coercion TyCon
64 -- We pass the Name of the parent TyCon, as well as the TyCon itself,
65 -- because the latter is part of a knot, whereas the former is not.
66 mkNewTyConRhs tycon_name tycon con
67 = do { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc
68 ; let co_tycon = mkNewTypeCo co_tycon_name tycon etad_tvs etad_roles etad_rhs
69 ; traceIf (text "mkNewTyConRhs" <+> ppr co_tycon)
70 ; return (NewTyCon { data_con = con,
71 nt_rhs = rhs_ty,
72 nt_etad_rhs = (etad_tvs, etad_rhs),
73 nt_co = co_tycon } ) }
74 -- Coreview looks through newtypes with a Nothing
75 -- for nt_co, or uses explicit coercions otherwise
76 where
77 tvs = tyConTyVars tycon
78 roles = tyConRoles tycon
79 inst_con_ty = applyTys (dataConUserType con) (mkTyVarTys tvs)
80 rhs_ty = ASSERT( isFunTy inst_con_ty ) funArgTy inst_con_ty
81 -- Instantiate the data con with the
82 -- type variables from the tycon
83 -- NB: a newtype DataCon has a type that must look like
84 -- forall tvs. <arg-ty> -> T tvs
85 -- Note that we *can't* use dataConInstOrigArgTys here because
86 -- the newtype arising from class Foo a => Bar a where {}
87 -- has a single argument (Foo a) that is a *type class*, so
88 -- dataConInstOrigArgTys returns [].
89
90 etad_tvs :: [TyVar] -- Matched lazily, so that mkNewTypeCo can
91 etad_roles :: [Role] -- return a TyCon without pulling on rhs_ty
92 etad_rhs :: Type -- See Note [Tricky iface loop] in LoadIface
93 (etad_tvs, etad_roles, etad_rhs) = eta_reduce (reverse tvs) (reverse roles) rhs_ty
94
95 eta_reduce :: [TyVar] -- Reversed
96 -> [Role] -- also reversed
97 -> Type -- Rhs type
98 -> ([TyVar], [Role], Type) -- Eta-reduced version
99 -- (tyvars in normal order)
100 eta_reduce (a:as) (_:rs) ty | Just (fun, arg) <- splitAppTy_maybe ty,
101 Just tv <- getTyVar_maybe arg,
102 tv == a,
103 not (a `elemVarSet` tyCoVarsOfType fun)
104 = eta_reduce as rs fun
105 eta_reduce tvs rs ty = (reverse tvs, reverse rs, ty)
106
107 ------------------------------------------------------
108 buildDataCon :: FamInstEnvs
109 -> Name
110 -> Bool -- Declared infix
111 -> TyConRepName
112 -> [HsSrcBang]
113 -> Maybe [HsImplBang]
114 -- See Note [Bangs on imported data constructors] in MkId
115 -> [FieldLabel] -- Field labels
116 -> [TyVar] -> [TyVar] -- Univ and ext
117 -> [EqSpec] -- Equality spec
118 -> ThetaType -- Does not include the "stupid theta"
119 -- or the GADT equalities
120 -> [Type] -> Type -- Argument and result types
121 -> TyCon -- Rep tycon
122 -> TcRnIf m n DataCon
123 -- A wrapper for DataCon.mkDataCon that
124 -- a) makes the worker Id
125 -- b) makes the wrapper Id if necessary, including
126 -- allocating its unique (hence monadic)
127 buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs field_lbls
128 univ_tvs ex_tvs eq_spec ctxt arg_tys res_ty rep_tycon
129 = do { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc
130 ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
131 -- This last one takes the name of the data constructor in the source
132 -- code, which (for Haskell source anyway) will be in the DataName name
133 -- space, and puts it into the VarName name space
134
135 ; traceIf (text "buildDataCon 1" <+> ppr src_name)
136 ; us <- newUniqueSupply
137 ; dflags <- getDynFlags
138 ; let
139 stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
140 data_con = mkDataCon src_name declared_infix prom_info
141 src_bangs field_lbls
142 univ_tvs ex_tvs eq_spec ctxt
143 arg_tys res_ty rep_tycon
144 stupid_ctxt dc_wrk dc_rep
145 dc_wrk = mkDataConWorkId work_name data_con
146 dc_rep = initUs_ us (mkDataConRep dflags fam_envs wrap_name
147 impl_bangs data_con)
148
149 ; traceIf (text "buildDataCon 2" <+> ppr src_name)
150 ; return data_con }
151
152
153 -- The stupid context for a data constructor should be limited to
154 -- the type variables mentioned in the arg_tys
155 -- ToDo: Or functionally dependent on?
156 -- This whole stupid theta thing is, well, stupid.
157 mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
158 mkDataConStupidTheta tycon arg_tys univ_tvs
159 | null stupid_theta = [] -- The common case
160 | otherwise = filter in_arg_tys stupid_theta
161 where
162 tc_subst = zipTopTCvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
163 stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
164 -- Start by instantiating the master copy of the
165 -- stupid theta, taken from the TyCon
166
167 arg_tyvars = tyCoVarsOfTypes arg_tys
168 in_arg_tys pred = not $ isEmptyVarSet $
169 tyCoVarsOfType pred `intersectVarSet` arg_tyvars
170
171
172 ------------------------------------------------------
173 buildPatSyn :: Name -> Bool
174 -> (Id,Bool) -> Maybe (Id, Bool)
175 -> ([TyVar], ThetaType) -- ^ Univ and req
176 -> ([TyVar], ThetaType) -- ^ Ex and prov
177 -> [Type] -- ^ Argument types
178 -> Type -- ^ Result type
179 -> [FieldLabel] -- ^ Field labels for
180 -- a record pattern synonym
181 -> PatSyn
182 buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
183 (univ_tvs, req_theta) (ex_tvs, prov_theta) arg_tys
184 pat_ty field_labels
185 = ASSERT2((and [ univ_tvs == univ_tvs1
186 , ex_tvs == ex_tvs1
187 , pat_ty `eqType` pat_ty1
188 , prov_theta `eqTypes` prov_theta1
189 , req_theta `eqTypes` req_theta1
190 , arg_tys `eqTypes` arg_tys1
191 ])
192 , (vcat [ ppr univ_tvs <+> twiddle <+> ppr univ_tvs1
193 , ppr ex_tvs <+> twiddle <+> ppr ex_tvs1
194 , ppr pat_ty <+> twiddle <+> ppr pat_ty1
195 , ppr prov_theta <+> twiddle <+> ppr prov_theta1
196 , ppr req_theta <+> twiddle <+> ppr req_theta1
197 , ppr arg_tys <+> twiddle <+> ppr arg_tys1]))
198 mkPatSyn src_name declared_infix
199 (univ_tvs, req_theta) (ex_tvs, prov_theta)
200 arg_tys pat_ty
201 matcher builder field_labels
202 where
203 ((_:_:univ_tvs1), req_theta1, tau) = tcSplitSigmaTy $ idType matcher_id
204 ([pat_ty1, cont_sigma, _], _) = tcSplitFunTys tau
205 (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy cont_sigma
206 (arg_tys1, _) = tcSplitFunTys cont_tau
207 twiddle = char '~'
208
209 ------------------------------------------------------
210 type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type))
211 -- A temporary intermediate, to communicate between
212 -- tcClassSigs and buildClass.
213
214 buildClass :: Name -- Name of the class/tycon (they have the same Name)
215 -> [TyVar] -> [Role] -> ThetaType
216 -> Kind
217 -> [FunDep TyVar] -- Functional dependencies
218 -> [ClassATItem] -- Associated types
219 -> [TcMethInfo] -- Method info
220 -> ClassMinimalDef -- Minimal complete definition
221 -> RecFlag -- Info for type constructor
222 -> TcRnIf m n Class
223
224 buildClass tycon_name tvs roles sc_theta kind fds at_items sig_stuff mindef tc_isrec
225 = fixM $ \ rec_clas -> -- Only name generation inside loop
226 do { traceIf (text "buildClass")
227
228 ; datacon_name <- newImplicitBinder tycon_name mkClassDataConOcc
229 ; tc_rep_name <- newTyConRepName tycon_name
230
231 ; op_items <- mapM (mk_op_item rec_clas) sig_stuff
232 -- Build the selector id and default method id
233
234 -- Make selectors for the superclasses
235 ; sc_sel_names <- mapM (newImplicitBinder tycon_name . mkSuperDictSelOcc)
236 (takeList sc_theta [fIRST_TAG..])
237 ; let sc_sel_ids = [ mkDictSelId sc_name rec_clas
238 | sc_name <- sc_sel_names]
239 -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
240 -- can construct names for the selectors. Thus
241 -- class (C a, C b) => D a b where ...
242 -- gives superclass selectors
243 -- D_sc1, D_sc2
244 -- (We used to call them D_C, but now we can have two different
245 -- superclasses both called C!)
246
247 ; let use_newtype = isSingleton arg_tys
248 -- Use a newtype if the data constructor
249 -- (a) has exactly one value field
250 -- i.e. exactly one operation or superclass taken together
251 -- (b) that value is of lifted type (which they always are, because
252 -- we box equality superclasses)
253 -- See note [Class newtypes and equality predicates]
254
255 -- We treat the dictionary superclasses as ordinary arguments.
256 -- That means that in the case of
257 -- class C a => D a
258 -- we don't get a newtype with no arguments!
259 args = sc_sel_names ++ op_names
260 op_tys = [ty | (_,ty,_) <- sig_stuff]
261 op_names = [op | (op,_,_) <- sig_stuff]
262 arg_tys = sc_theta ++ op_tys
263 rec_tycon = classTyCon rec_clas
264
265 ; rep_nm <- newTyConRepName datacon_name
266 ; dict_con <- buildDataCon (panic "buildClass: FamInstEnvs")
267 datacon_name
268 False -- Not declared infix
269 rep_nm
270 (map (const no_bang) args)
271 (Just (map (const HsLazy) args))
272 [{- No fields -}]
273 tvs [{- no existentials -}]
274 [{- No GADT equalities -}]
275 [{- No theta -}]
276 arg_tys
277 (mkTyConApp rec_tycon (mkTyVarTys tvs))
278 rec_tycon
279
280 ; rhs <- if use_newtype
281 then mkNewTyConRhs tycon_name rec_tycon dict_con
282 else if isCTupleTyConName tycon_name
283 then return (TupleTyCon { data_con = dict_con
284 , tup_sort = ConstraintTuple })
285 else return (mkDataTyConRhs [dict_con])
286
287 ; let { tycon = mkClassTyCon tycon_name kind tvs roles
288 rhs rec_clas tc_isrec tc_rep_name
289 -- A class can be recursive, and in the case of newtypes
290 -- this matters. For example
291 -- class C a where { op :: C b => a -> b -> Int }
292 -- Because C has only one operation, it is represented by
293 -- a newtype, and it should be a *recursive* newtype.
294 -- [If we don't make it a recursive newtype, we'll expand the
295 -- newtype like a synonym, but that will lead to an infinite
296 -- type]
297
298 ; result = mkClass tvs fds
299 sc_theta sc_sel_ids at_items
300 op_items mindef tycon
301 }
302 ; traceIf (text "buildClass" <+> ppr tycon)
303 ; return result }
304 where
305 no_bang = HsSrcBang Nothing NoSrcUnpack NoSrcStrict
306
307 mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
308 mk_op_item rec_clas (op_name, _, dm_spec)
309 = do { dm_info <- case dm_spec of
310 Nothing -> return Nothing
311 Just spec -> do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
312 ; return (Just (dm_name, spec)) }
313 ; return (mkDictSelId op_name rec_clas, dm_info) }
314
315 {-
316 Note [Class newtypes and equality predicates]
317 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
318 Consider
319 class (a ~ F b) => C a b where
320 op :: a -> b
321
322 We cannot represent this by a newtype, even though it's not
323 existential, because there are two value fields (the equality
324 predicate and op. See Trac #2238
325
326 Moreover,
327 class (a ~ F b) => C a b where {}
328 Here we can't use a newtype either, even though there is only
329 one field, because equality predicates are unboxed, and classes
330 are boxed.
331 -}
332
333 newImplicitBinder :: Name -- Base name
334 -> (OccName -> OccName) -- Occurrence name modifier
335 -> TcRnIf m n Name -- Implicit name
336 -- Called in BuildTyCl to allocate the implicit binders of type/class decls
337 -- For source type/class decls, this is the first occurrence
338 -- For iface ones, the LoadIface has alrady allocated a suitable name in the cache
339 newImplicitBinder base_name mk_sys_occ
340 | Just mod <- nameModule_maybe base_name
341 = newGlobalBinder mod occ loc
342 | otherwise -- When typechecking a [d| decl bracket |],
343 -- TH generates types, classes etc with Internal names,
344 -- so we follow suit for the implicit binders
345 = do { uniq <- newUnique
346 ; return (mkInternalName uniq occ loc) }
347 where
348 occ = mk_sys_occ (nameOccName base_name)
349 loc = nameSrcSpan base_name
350
351 -- | Make the 'TyConRepName' for this 'TyCon'
352 newTyConRepName :: Name -> TcRnIf gbl lcl TyConRepName
353 newTyConRepName tc_name
354 | Just mod <- nameModule_maybe tc_name
355 , (mod, occ) <- tyConRepModOcc mod (nameOccName tc_name)
356 = newGlobalBinder mod occ noSrcSpan
357 | otherwise
358 = newImplicitBinder tc_name mkTyConRepUserOcc