never executed always true always false
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 -}
5
6
7
8 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
9
10 module GHC.Tc.TyCl.Build (
11 buildDataCon,
12 buildPatSyn,
13 TcMethInfo, MethInfo, buildClass,
14 mkNewTyConRhs,
15 newImplicitBinder, newTyConRepName
16 ) where
17
18 import GHC.Prelude
19
20 import GHC.Iface.Env
21 import GHC.Core.FamInstEnv( FamInstEnvs, mkNewTypeCoAxiom )
22 import GHC.Builtin.Types( isCTupleTyConName, unboxedUnitTy )
23 import GHC.Core.DataCon
24 import GHC.Core.PatSyn
25 import GHC.Types.Var
26 import GHC.Types.Var.Set
27 import GHC.Types.Basic
28 import GHC.Types.Name
29 import GHC.Types.Name.Env
30 import GHC.Types.Id.Make
31 import GHC.Core.Class
32 import GHC.Core.TyCon
33 import GHC.Core.Type
34 import GHC.Types.SourceText
35 import GHC.Tc.Utils.TcType
36 import GHC.Core.Multiplicity
37
38 import GHC.Types.SrcLoc( SrcSpan, noSrcSpan )
39 import GHC.Driver.Session
40 import GHC.Tc.Utils.Monad
41 import GHC.Types.Unique.Supply
42 import GHC.Utils.Misc
43 import GHC.Utils.Outputable
44 import GHC.Utils.Panic
45
46
47 mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
48 -- ^ Monadic because it makes a Name for the coercion TyCon
49 -- We pass the Name of the parent TyCon, as well as the TyCon itself,
50 -- because the latter is part of a knot, whereas the former is not.
51 mkNewTyConRhs tycon_name tycon con
52 = do { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc
53 ; let nt_ax = mkNewTypeCoAxiom co_tycon_name tycon etad_tvs etad_roles etad_rhs
54 ; traceIf (text "mkNewTyConRhs" <+> ppr nt_ax)
55 ; return (NewTyCon { data_con = con,
56 nt_rhs = rhs_ty,
57 nt_etad_rhs = (etad_tvs, etad_rhs),
58 nt_co = nt_ax,
59 nt_fixed_rep = isFixedRuntimeRepKind res_kind } ) }
60 -- Coreview looks through newtypes with a Nothing
61 -- for nt_co, or uses explicit coercions otherwise
62 where
63 tvs = tyConTyVars tycon
64 roles = tyConRoles tycon
65 res_kind = tyConResKind tycon
66 con_arg_ty = case dataConRepArgTys con of
67 [arg_ty] -> scaledThing arg_ty
68 tys -> pprPanic "mkNewTyConRhs" (ppr con <+> ppr tys)
69 rhs_ty = substTyWith (dataConUnivTyVars con)
70 (mkTyVarTys tvs) con_arg_ty
71 -- Instantiate the newtype's RHS with the
72 -- type variables from the tycon
73 -- NB: a newtype DataCon has a type that must look like
74 -- forall tvs. <arg-ty> -> T tvs
75 -- Note that we *can't* use dataConInstOrigArgTys here because
76 -- the newtype arising from class Foo a => Bar a where {}
77 -- has a single argument (Foo a) that is a *type class*, so
78 -- dataConInstOrigArgTys returns [].
79
80 -- Eta-reduce the newtype
81 -- See Note [Newtype eta] in GHC.Core.TyCon
82 etad_tvs :: [TyVar] -- Matched lazily, so that mkNewTypeCo can
83 etad_roles :: [Role] -- return a TyCon without pulling on rhs_ty
84 etad_rhs :: Type -- See Note [Tricky iface loop] in GHC.Iface.Load
85 (etad_tvs, etad_roles, etad_rhs) = eta_reduce (reverse tvs) (reverse roles) rhs_ty
86
87 eta_reduce :: [TyVar] -- Reversed
88 -> [Role] -- also reversed
89 -> Type -- Rhs type
90 -> ([TyVar], [Role], Type) -- Eta-reduced version
91 -- (tyvars in normal order)
92 eta_reduce (a:as) (_:rs) ty
93 | Just (fun, arg) <- splitAppTy_maybe ty
94 , Just tv <- getTyVar_maybe arg
95 , tv == a
96 , not (a `elemVarSet` tyCoVarsOfType fun)
97 , typeKind fun `eqType` typeKind (mkTyConApp tycon (mkTyVarTys $ reverse as))
98 -- Why this kind-check? See Note [Newtype eta and homogeneous axioms]
99 = eta_reduce as rs fun
100 eta_reduce as rs ty = (reverse as, reverse rs, ty)
101
102 {- Note [Newtype eta and homogeneous axioms]
103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
104 When eta-reducing a newtype, we must be careful to make sure the axiom
105 is homogeneous. (That is, the two types related by the axiom must
106 have the same kind.) All known proofs of type safety for Core rely on
107 the homogeneity of axioms, so let's not monkey with that.
108
109 It is easy to mistakenly make an inhomogeneous axiom (#19739):
110 type T :: forall (a :: Type) -> Type
111 newtype T a = MkT (Proxy a)
112
113 Can we eta-reduce, thus?
114 axT :: T ~ Proxy
115
116 No! Because
117 T :: forall a -> Type
118 Proxy :: Type -> Type
119
120 This is inhomogeneous. Hence, we have an extra kind-check in eta_reduce,
121 to make sure the reducts have the same kind. This is simple, although
122 perhaps quadratic in complexity, if we eta-reduce many arguments (which
123 seems vanishingly unlikely in practice). But NB that the free-variable
124 check, which immediately precedes the kind check, is also potentially
125 quadratic.
126
127 There are other ways we could do the check (discussion on #19739):
128
129 * We could look at the sequence of binders on the newtype and on the
130 head of the representation type, and make sure the visibilities on
131 the binders match up. This is quite a bit more code, and the reasoning
132 is subtler.
133
134 * We could, say, do the kind-check at the end and then backtrack until the
135 kinds match up. Hard to know whether that's more performant or not.
136 -}
137
138 ------------------------------------------------------
139 buildDataCon :: FamInstEnvs
140 -> Name
141 -> Bool -- Declared infix
142 -> TyConRepName
143 -> [HsSrcBang]
144 -> Maybe [HsImplBang]
145 -- See Note [Bangs on imported data constructors] in GHC.Types.Id.Make
146 -> [FieldLabel] -- Field labels
147 -> [TyVar] -- Universals
148 -> [TyCoVar] -- Existentials
149 -> [InvisTVBinder] -- User-written 'TyVarBinder's
150 -> [EqSpec] -- Equality spec
151 -> KnotTied ThetaType -- Does not include the "stupid theta"
152 -- or the GADT equalities
153 -> [KnotTied (Scaled Type)] -- Arguments
154 -> KnotTied Type -- Result types
155 -> KnotTied TyCon -- Rep tycon
156 -> NameEnv ConTag -- Maps the Name of each DataCon to its
157 -- ConTag
158 -> TcRnIf m n DataCon
159 -- A wrapper for DataCon.mkDataCon that
160 -- a) makes the worker Id
161 -- b) makes the wrapper Id if necessary, including
162 -- allocating its unique (hence monadic)
163 buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs
164 field_lbls univ_tvs ex_tvs user_tvbs eq_spec ctxt arg_tys res_ty
165 rep_tycon tag_map
166 = do { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc
167 ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
168 -- This last one takes the name of the data constructor in the source
169 -- code, which (for Haskell source anyway) will be in the DataName name
170 -- space, and puts it into the VarName name space
171
172 ; traceIf (text "buildDataCon 1" <+> ppr src_name)
173 ; us <- newUniqueSupply
174 ; dflags <- getDynFlags
175 ; let stupid_ctxt = mkDataConStupidTheta rep_tycon (map scaledThing arg_tys) univ_tvs
176 tag = lookupNameEnv_NF tag_map src_name
177 -- See Note [Constructor tag allocation], fixes #14657
178 data_con = mkDataCon src_name declared_infix prom_info
179 src_bangs field_lbls
180 univ_tvs ex_tvs user_tvbs eq_spec ctxt
181 arg_tys res_ty NoRRI rep_tycon tag
182 stupid_ctxt dc_wrk dc_rep
183 dc_wrk = mkDataConWorkId work_name data_con
184 dc_rep = initUs_ us (mkDataConRep dflags fam_envs wrap_name
185 impl_bangs data_con)
186
187 ; traceIf (text "buildDataCon 2" <+> ppr src_name)
188 ; return data_con }
189
190
191 -- The stupid context for a data constructor should be limited to
192 -- the type variables mentioned in the arg_tys
193 -- ToDo: Or functionally dependent on?
194 -- This whole stupid theta thing is, well, stupid.
195 mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
196 mkDataConStupidTheta tycon arg_tys univ_tvs
197 | null stupid_theta = [] -- The common case
198 | otherwise = filter in_arg_tys stupid_theta
199 where
200 tc_subst = zipTvSubst (tyConTyVars tycon)
201 (mkTyVarTys univ_tvs)
202 stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
203 -- Start by instantiating the master copy of the
204 -- stupid theta, taken from the TyCon
205
206 arg_tyvars = tyCoVarsOfTypes arg_tys
207 in_arg_tys pred = tyCoVarsOfType pred `intersectsVarSet` arg_tyvars
208
209
210 ------------------------------------------------------
211 buildPatSyn :: Name -> Bool
212 -> PatSynMatcher -> PatSynBuilder
213 -> ([InvisTVBinder], ThetaType) -- ^ Univ and req
214 -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov
215 -> [Type] -- ^ Argument types
216 -> Type -- ^ Result type
217 -> [FieldLabel] -- ^ Field labels for
218 -- a record pattern synonym
219 -> PatSyn
220 buildPatSyn src_name declared_infix matcher@(_, matcher_ty,_) builder
221 (univ_tvs, req_theta) (ex_tvs, prov_theta) arg_tys
222 pat_ty field_labels
223 = -- The assertion checks that the matcher is
224 -- compatible with the pattern synonym
225 assertPpr (and [ univ_tvs `equalLength` univ_tvs1
226 , ex_tvs `equalLength` ex_tvs1
227 , pat_ty `eqType` substTy subst (scaledThing pat_ty1)
228 , prov_theta `eqTypes` substTys subst prov_theta1
229 , req_theta `eqTypes` substTys subst req_theta1
230 , compareArgTys arg_tys (substTys subst (map scaledThing arg_tys1))
231 ])
232 (vcat [ ppr univ_tvs <+> twiddle <+> ppr univ_tvs1
233 , ppr ex_tvs <+> twiddle <+> ppr ex_tvs1
234 , ppr pat_ty <+> twiddle <+> ppr pat_ty1
235 , ppr prov_theta <+> twiddle <+> ppr prov_theta1
236 , ppr req_theta <+> twiddle <+> ppr req_theta1
237 , ppr arg_tys <+> twiddle <+> ppr arg_tys1]) $
238 mkPatSyn src_name declared_infix
239 (univ_tvs, req_theta) (ex_tvs, prov_theta)
240 arg_tys pat_ty
241 matcher builder field_labels
242 where
243 ((_:_:univ_tvs1), req_theta1, tau) = tcSplitSigmaTy $ matcher_ty
244 ([pat_ty1, cont_sigma, _], _) = tcSplitFunTys tau
245 (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy (scaledThing cont_sigma)
246 (arg_tys1, _) = (tcSplitFunTys cont_tau)
247 twiddle = char '~'
248 subst = zipTvSubst (univ_tvs1 ++ ex_tvs1)
249 (mkTyVarTys (binderVars (univ_tvs ++ ex_tvs)))
250
251 -- For a nullary pattern synonym we add a single (# #) argument to the
252 -- matcher to preserve laziness in the case of unlifted types.
253 -- See #12746
254 compareArgTys :: [Type] -> [Type] -> Bool
255 compareArgTys [] [x] = x `eqType` unboxedUnitTy
256 compareArgTys arg_tys matcher_arg_tys = arg_tys `eqTypes` matcher_arg_tys
257
258
259 ------------------------------------------------------
260 type TcMethInfo = MethInfo -- this variant needs zonking
261 type MethInfo -- A temporary intermediate, to communicate
262 -- between tcClassSigs and buildClass.
263 = ( Name -- Name of the class op
264 , Type -- Type of the class op
265 , Maybe (DefMethSpec (SrcSpan, Type)))
266 -- Nothing => no default method
267 --
268 -- Just VanillaDM => There is an ordinary
269 -- polymorphic default method
270 --
271 -- Just (GenericDM (loc, ty)) => There is a generic default metho
272 -- Here is its type, and the location
273 -- of the type signature
274 -- We need that location /only/ to attach it to the
275 -- generic default method's Name; and we need /that/
276 -- only to give the right location of an ambiguity error
277 -- for the generic default method, spat out by checkValidClass
278
279 buildClass :: Name -- Name of the class/tycon (they have the same Name)
280 -> [TyConBinder] -- Of the tycon
281 -> [Role]
282 -> [FunDep TyVar] -- Functional dependencies
283 -- Super classes, associated types, method info, minimal complete def.
284 -- This is Nothing if the class is abstract.
285 -> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
286 -> TcRnIf m n Class
287
288 buildClass tycon_name binders roles fds Nothing
289 = fixM $ \ rec_clas -> -- Only name generation inside loop
290 do { traceIf (text "buildClass")
291
292 ; tc_rep_name <- newTyConRepName tycon_name
293 ; let univ_tvs = binderVars binders
294 tycon = mkClassTyCon tycon_name binders roles
295 AbstractTyCon
296 rec_clas tc_rep_name
297 result = mkAbstractClass tycon_name univ_tvs fds tycon
298 ; traceIf (text "buildClass" <+> ppr tycon)
299 ; return result }
300
301 buildClass tycon_name binders roles fds
302 (Just (sc_theta, at_items, sig_stuff, mindef))
303 = fixM $ \ rec_clas -> -- Only name generation inside loop
304 do { traceIf (text "buildClass")
305
306 ; datacon_name <- newImplicitBinder tycon_name mkClassDataConOcc
307 ; tc_rep_name <- newTyConRepName tycon_name
308
309 ; op_items <- mapM (mk_op_item rec_clas) sig_stuff
310 -- Build the selector id and default method id
311
312 -- Make selectors for the superclasses
313 ; sc_sel_names <- mapM (newImplicitBinder tycon_name . mkSuperDictSelOcc)
314 (takeList sc_theta [fIRST_TAG..])
315 ; let sc_sel_ids = [ mkDictSelId sc_name rec_clas
316 | sc_name <- sc_sel_names]
317 -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
318 -- can construct names for the selectors. Thus
319 -- class (C a, C b) => D a b where ...
320 -- gives superclass selectors
321 -- D_sc1, D_sc2
322 -- (We used to call them D_C, but now we can have two different
323 -- superclasses both called C!)
324
325 ; let use_newtype = isSingleton arg_tys
326 -- Use a newtype if the data constructor
327 -- (a) has exactly one value field
328 -- i.e. exactly one operation or superclass taken together
329 -- (b) that value is of lifted type (which they always are, because
330 -- we box equality superclasses)
331 -- See note [Class newtypes and equality predicates]
332
333 -- We treat the dictionary superclasses as ordinary arguments.
334 -- That means that in the case of
335 -- class C a => D a
336 -- we don't get a newtype with no arguments!
337 args = sc_sel_names ++ op_names
338 op_tys = [ty | (_,ty,_) <- sig_stuff]
339 op_names = [op | (op,_,_) <- sig_stuff]
340 arg_tys = sc_theta ++ op_tys
341 rec_tycon = classTyCon rec_clas
342 univ_bndrs = tyConInvisTVBinders binders
343 univ_tvs = binderVars univ_bndrs
344
345 ; rep_nm <- newTyConRepName datacon_name
346 ; dict_con <- buildDataCon (panic "buildClass: FamInstEnvs")
347 datacon_name
348 False -- Not declared infix
349 rep_nm
350 (map (const no_bang) args)
351 (Just (map (const HsLazy) args))
352 [{- No fields -}]
353 univ_tvs
354 [{- no existentials -}]
355 univ_bndrs
356 [{- No GADT equalities -}]
357 [{- No theta -}]
358 (map unrestricted arg_tys) -- type classes are unrestricted
359 (mkTyConApp rec_tycon (mkTyVarTys univ_tvs))
360 rec_tycon
361 (mkTyConTagMap rec_tycon)
362
363 ; rhs <- case () of
364 _ | use_newtype
365 -> mkNewTyConRhs tycon_name rec_tycon dict_con
366 | isCTupleTyConName tycon_name
367 -> return (TupleTyCon { data_con = dict_con
368 , tup_sort = ConstraintTuple })
369 | otherwise
370 -> return (mkDataTyConRhs [dict_con])
371
372 ; let { tycon = mkClassTyCon tycon_name binders roles
373 rhs rec_clas tc_rep_name
374 -- A class can be recursive, and in the case of newtypes
375 -- this matters. For example
376 -- class C a where { op :: C b => a -> b -> Int }
377 -- Because C has only one operation, it is represented by
378 -- a newtype, and it should be a *recursive* newtype.
379 -- [If we don't make it a recursive newtype, we'll expand the
380 -- newtype like a synonym, but that will lead to an infinite
381 -- type]
382
383 ; result = mkClass tycon_name univ_tvs fds
384 sc_theta sc_sel_ids at_items
385 op_items mindef tycon
386 }
387 ; traceIf (text "buildClass" <+> ppr tycon)
388 ; return result }
389 where
390 no_bang = HsSrcBang NoSourceText NoSrcUnpack NoSrcStrict
391
392 mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
393 mk_op_item rec_clas (op_name, _, dm_spec)
394 = do { dm_info <- mk_dm_info op_name dm_spec
395 ; return (mkDictSelId op_name rec_clas, dm_info) }
396
397 mk_dm_info :: Name -> Maybe (DefMethSpec (SrcSpan, Type))
398 -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
399 mk_dm_info _ Nothing
400 = return Nothing
401 mk_dm_info op_name (Just VanillaDM)
402 = do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
403 ; return (Just (dm_name, VanillaDM)) }
404 mk_dm_info op_name (Just (GenericDM (loc, dm_ty)))
405 = do { dm_name <- newImplicitBinderLoc op_name mkDefaultMethodOcc loc
406 ; return (Just (dm_name, GenericDM dm_ty)) }
407
408 {-
409 Note [Class newtypes and equality predicates]
410 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
411 Consider
412 class (a ~ F b) => C a b where
413 op :: a -> b
414
415 We cannot represent this by a newtype, even though it's not
416 existential, because there are two value fields (the equality
417 predicate and op. See #2238
418
419 Moreover,
420 class (a ~ F b) => C a b where {}
421 Here we can't use a newtype either, even though there is only
422 one field, because equality predicates are unboxed, and classes
423 are boxed.
424 -}
425
426 newImplicitBinder :: Name -- Base name
427 -> (OccName -> OccName) -- Occurrence name modifier
428 -> TcRnIf m n Name -- Implicit name
429 -- Called in GHC.Tc.TyCl.Build to allocate the implicit binders of type/class decls
430 -- For source type/class decls, this is the first occurrence
431 -- For iface ones, GHC.Iface.Load has already allocated a suitable name in the cache
432 newImplicitBinder base_name mk_sys_occ
433 = newImplicitBinderLoc base_name mk_sys_occ (nameSrcSpan base_name)
434
435 newImplicitBinderLoc :: Name -- Base name
436 -> (OccName -> OccName) -- Occurrence name modifier
437 -> SrcSpan
438 -> TcRnIf m n Name -- Implicit name
439 -- Just the same, but lets you specify the SrcSpan
440 newImplicitBinderLoc base_name mk_sys_occ loc
441 | Just mod <- nameModule_maybe base_name
442 = newGlobalBinder mod occ loc
443 | otherwise -- When typechecking a [d| decl bracket |],
444 -- TH generates types, classes etc with Internal names,
445 -- so we follow suit for the implicit binders
446 = do { uniq <- newUnique
447 ; return (mkInternalName uniq occ loc) }
448 where
449 occ = mk_sys_occ (nameOccName base_name)
450
451 -- | Make the 'TyConRepName' for this 'TyCon'
452 newTyConRepName :: Name -> TcRnIf gbl lcl TyConRepName
453 newTyConRepName tc_name
454 | Just mod <- nameModule_maybe tc_name
455 , (mod, occ) <- tyConRepModOcc mod (nameOccName tc_name)
456 = newGlobalBinder mod occ noSrcSpan
457 | otherwise
458 = newImplicitBinder tc_name mkTyConRepOcc