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 {-# LANGUAGE FlexibleContexts #-}
9 {-# LANGUAGE TypeFamilies #-}
10
11 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
12 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
13
14 -- | Typechecking instance declarations
15 module GHC.Tc.TyCl.Instance
16 ( tcInstDecls1
17 , tcInstDeclsDeriv
18 , tcInstDecls2
19 )
20 where
21
22 import GHC.Prelude
23
24 import GHC.Hs
25 import GHC.Tc.Errors.Types
26 import GHC.Tc.Gen.Bind
27 import GHC.Tc.TyCl
28 import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv )
29 import GHC.Tc.TyCl.Class ( tcClassDecl2, ClassScopedTVEnv, tcATDefault,
30 HsSigFun, mkHsSigFun, badMethodErr,
31 findMethodBind, instantiateMethod )
32 import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
33 import GHC.Tc.Gen.Sig
34 import GHC.Tc.Utils.Monad
35 import GHC.Tc.Validity
36 import GHC.Tc.Utils.Zonk
37 import GHC.Tc.Utils.TcMType
38 import GHC.Tc.Utils.TcType
39 import GHC.Tc.Types.Constraint
40 import GHC.Tc.Types.Origin
41 import GHC.Tc.TyCl.Build
42 import GHC.Tc.Utils.Instantiate
43 import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated )
44 import GHC.Core.Multiplicity
45 import GHC.Core.InstEnv
46 import GHC.Tc.Instance.Family
47 import GHC.Core.FamInstEnv
48 import GHC.Tc.Deriv
49 import GHC.Tc.Utils.Env
50 import GHC.Tc.Gen.HsType
51 import GHC.Tc.Utils.Unify
52 import GHC.Core ( Expr(..), mkApps, mkVarApps, mkLams )
53 import GHC.Core.Make ( nO_METHOD_BINDING_ERROR_ID )
54 import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
55 import GHC.Core.Type
56 import GHC.Core.SimpleOpt
57 import GHC.Core.Predicate( classMethodInstTy )
58 import GHC.Tc.Types.Evidence
59 import GHC.Core.TyCon
60 import GHC.Core.Coercion.Axiom
61 import GHC.Core.DataCon
62 import GHC.Core.ConLike
63 import GHC.Core.Class
64 import GHC.Types.Error
65 import GHC.Types.Var as Var
66 import GHC.Types.Var.Env
67 import GHC.Types.Var.Set
68 import GHC.Data.Bag
69 import GHC.Types.Basic
70 import GHC.Types.Fixity
71 import GHC.Driver.Session
72 import GHC.Driver.Ppr
73 import GHC.Utils.Logger
74 import GHC.Data.FastString
75 import GHC.Types.Id
76 import GHC.Types.SourceText
77 import GHC.Data.List.SetOps
78 import GHC.Types.Name
79 import GHC.Types.Name.Set
80 import GHC.Utils.Outputable
81 import GHC.Utils.Panic
82 import GHC.Utils.Panic.Plain
83 import GHC.Types.SrcLoc
84 import GHC.Utils.Misc
85 import GHC.Data.BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
86 import qualified GHC.LanguageExtensions as LangExt
87
88 import Control.Monad
89 import Data.Tuple
90 import GHC.Data.Maybe
91 import Data.List( mapAccumL )
92
93
94 {-
95 Typechecking instance declarations is done in two passes. The first
96 pass, made by @tcInstDecls1@, collects information to be used in the
97 second pass.
98
99 This pre-processed info includes the as-yet-unprocessed bindings
100 inside the instance declaration. These are type-checked in the second
101 pass, when the class-instance envs and GVE contain all the info from
102 all the instance and value decls. Indeed that's the reason we need
103 two passes over the instance decls.
104
105
106 Note [How instance declarations are translated]
107 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
108 Here is how we translate instance declarations into Core
109
110 Running example:
111 class C a where
112 op1, op2 :: Ix b => a -> b -> b
113 op2 = <dm-rhs>
114
115 instance C a => C [a]
116 {-# INLINE [2] op1 #-}
117 op1 = <rhs>
118 ===>
119 -- Method selectors
120 op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
121 op1 = ...
122 op2 = ...
123
124 -- Default methods get the 'self' dictionary as argument
125 -- so they can call other methods at the same type
126 -- Default methods get the same type as their method selector
127 $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
128 $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
129 -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
130 -- Note [Tricky type variable scoping]
131
132 -- A top-level definition for each instance method
133 -- Here op1_i, op2_i are the "instance method Ids"
134 -- The INLINE pragma comes from the user pragma
135 {-# INLINE [2] op1_i #-} -- From the instance decl bindings
136 op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
137 op1_i = /\a. \(d:C a).
138 let this :: C [a]
139 this = df_i a d
140 -- Note [Subtle interaction of recursion and overlap]
141
142 local_op1 :: forall b. Ix b => [a] -> b -> b
143 local_op1 = <rhs>
144 -- Source code; run the type checker on this
145 -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
146 -- Note [Tricky type variable scoping]
147
148 in local_op1 a d
149
150 op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
151
152 -- The dictionary function itself
153 {-# NOINLINE CONLIKE df_i #-} -- Never inline dictionary functions
154 df_i :: forall a. C a -> C [a]
155 df_i = /\a. \d:C a. MkC (op1_i a d) (op2_i a d)
156 -- But see Note [Default methods in instances]
157 -- We can't apply the type checker to the default-method call
158
159 -- Use a RULE to short-circuit applications of the class ops
160 {-# RULE "op1@C[a]" forall a, d:C a.
161 op1 [a] (df_i d) = op1_i a d #-}
162
163 Note [Instances and loop breakers]
164 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
165 * Note that df_i may be mutually recursive with both op1_i and op2_i.
166 It's crucial that df_i is not chosen as the loop breaker, even
167 though op1_i has a (user-specified) INLINE pragma.
168
169 * Instead the idea is to inline df_i into op1_i, which may then select
170 methods from the MkC record, and thereby break the recursion with
171 df_i, leaving a *self*-recursive op1_i. (If op1_i doesn't call op at
172 the same type, it won't mention df_i, so there won't be recursion in
173 the first place.)
174
175 * If op1_i is marked INLINE by the user there's a danger that we won't
176 inline df_i in it, and that in turn means that (since it'll be a
177 loop-breaker because df_i isn't), op1_i will ironically never be
178 inlined. But this is OK: the recursion breaking happens by way of
179 a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
180 unfoldings. See Note [RULEs enabled in InitialPhase] in GHC.Core.Opt.Simplify.Utils
181
182 Note [ClassOp/DFun selection]
183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
184 One thing we see a lot is stuff like
185 op2 (df d1 d2)
186 where 'op2' is a ClassOp and 'df' is DFun. Now, we could inline *both*
187 'op2' and 'df' to get
188 case (MkD ($cop1 d1 d2) ($cop2 d1 d2) ... of
189 MkD _ op2 _ _ _ -> op2
190 And that will reduce to ($cop2 d1 d2) which is what we wanted.
191
192 But it's tricky to make this work in practice, because it requires us to
193 inline both 'op2' and 'df'. But neither is keen to inline without having
194 seen the other's result; and it's very easy to get code bloat (from the
195 big intermediate) if you inline a bit too much.
196
197 Instead we use a cunning trick.
198 * We arrange that 'df' and 'op2' NEVER inline.
199
200 * We arrange that 'df' is ALWAYS defined in the sylised form
201 df d1 d2 = MkD ($cop1 d1 d2) ($cop2 d1 d2) ...
202
203 * We give 'df' a magical unfolding (DFunUnfolding [$cop1, $cop2, ..])
204 that lists its methods.
205
206 * We make GHC.Core.Unfold.exprIsConApp_maybe spot a DFunUnfolding and return
207 a suitable constructor application -- inlining df "on the fly" as it
208 were.
209
210 * ClassOp rules: We give the ClassOp 'op2' a BuiltinRule that
211 extracts the right piece iff its argument satisfies
212 exprIsConApp_maybe. This is done in GHC.Types.Id.Make.mkDictSelId
213
214 * We make 'df' CONLIKE, so that shared uses still match; eg
215 let d = df d1 d2
216 in ...(op2 d)...(op1 d)...
217
218 Note [Single-method classes]
219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
220 If the class has just one method (or, more accurately, just one element
221 of {superclasses + methods}), then we use a different strategy.
222
223 class C a where op :: a -> a
224 instance C a => C [a] where op = <blah>
225
226 We translate the class decl into a newtype, which just gives a
227 top-level axiom. The "constructor" MkC expands to a cast, as does the
228 class-op selector.
229
230 axiom Co:C a :: C a ~ (a->a)
231
232 op :: forall a. C a -> (a -> a)
233 op a d = d |> (Co:C a)
234
235 MkC :: forall a. (a->a) -> C a
236 MkC = /\a.\op. op |> (sym Co:C a)
237
238 The clever RULE stuff doesn't work now, because ($df a d) isn't
239 a constructor application, so exprIsConApp_maybe won't return
240 Just <blah>.
241
242 Instead, we simply rely on the fact that casts are cheap:
243
244 $df :: forall a. C a => C [a]
245 {-# INLINE df #-} -- NB: INLINE this
246 $df = /\a. \d. MkC [a] ($cop_list a d)
247 = $cop_list |> forall a. C a -> (sym (Co:C [a]))
248
249 $cop_list :: forall a. C a => [a] -> [a]
250 $cop_list = <blah>
251
252 So if we see
253 (op ($df a d))
254 we'll inline 'op' and '$df', since both are simply casts, and
255 good things happen.
256
257 Why do we use this different strategy? Because otherwise we
258 end up with non-inlined dictionaries that look like
259 $df = $cop |> blah
260 which adds an extra indirection to every use, which seems stupid. See
261 #4138 for an example (although the regression reported there
262 wasn't due to the indirection).
263
264 There is an awkward wrinkle though: we want to be very
265 careful when we have
266 instance C a => C [a] where
267 {-# INLINE op #-}
268 op = ...
269 then we'll get an INLINE pragma on $cop_list but it's important that
270 $cop_list only inlines when it's applied to *two* arguments (the
271 dictionary and the list argument). So we must not eta-expand $df
272 above. We ensure that this doesn't happen by putting an INLINE
273 pragma on the dfun itself; after all, it ends up being just a cast.
274
275 There is one more dark corner to the INLINE story, even more deeply
276 buried. Consider this (#3772):
277
278 class DeepSeq a => C a where
279 gen :: Int -> a
280
281 instance C a => C [a] where
282 gen n = ...
283
284 class DeepSeq a where
285 deepSeq :: a -> b -> b
286
287 instance DeepSeq a => DeepSeq [a] where
288 {-# INLINE deepSeq #-}
289 deepSeq xs b = foldr deepSeq b xs
290
291 That gives rise to these defns:
292
293 $cdeepSeq :: DeepSeq a -> [a] -> b -> b
294 -- User INLINE( 3 args )!
295 $cdeepSeq a (d:DS a) b (x:[a]) (y:b) = ...
296
297 $fDeepSeq[] :: DeepSeq a -> DeepSeq [a]
298 -- DFun (with auto INLINE pragma)
299 $fDeepSeq[] a d = $cdeepSeq a d |> blah
300
301 $cp1 a d :: C a => DeepSep [a]
302 -- We don't want to eta-expand this, lest
303 -- $cdeepSeq gets inlined in it!
304 $cp1 a d = $fDeepSep[] a (scsel a d)
305
306 $fC[] :: C a => C [a]
307 -- Ordinary DFun
308 $fC[] a d = MkC ($cp1 a d) ($cgen a d)
309
310 Here $cp1 is the code that generates the superclass for C [a]. The
311 issue is this: we must not eta-expand $cp1 either, or else $fDeepSeq[]
312 and then $cdeepSeq will inline there, which is definitely wrong. Like
313 on the dfun, we solve this by adding an INLINE pragma to $cp1.
314
315 Note [Subtle interaction of recursion and overlap]
316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
317 Consider this
318 class C a where { op1,op2 :: a -> a }
319 instance C a => C [a] where
320 op1 x = op2 x ++ op2 x
321 op2 x = ...
322 instance C [Int] where
323 ...
324
325 When type-checking the C [a] instance, we need a C [a] dictionary (for
326 the call of op2). If we look up in the instance environment, we find
327 an overlap. And in *general* the right thing is to complain (see Note
328 [Overlapping instances] in GHC.Core.InstEnv). But in *this* case it's wrong to
329 complain, because we just want to delegate to the op2 of this same
330 instance.
331
332 Why is this justified? Because we generate a (C [a]) constraint in
333 a context in which 'a' cannot be instantiated to anything that matches
334 other overlapping instances, or else we would not be executing this
335 version of op1 in the first place.
336
337 It might even be a bit disguised:
338
339 nullFail :: C [a] => [a] -> [a]
340 nullFail x = op2 x ++ op2 x
341
342 instance C a => C [a] where
343 op1 x = nullFail x
344
345 Precisely this is used in package 'regex-base', module Context.hs.
346 See the overlapping instances for RegexContext, and the fact that they
347 call 'nullFail' just like the example above. The DoCon package also
348 does the same thing; it shows up in module Fraction.hs.
349
350 Conclusion: when typechecking the methods in a C [a] instance, we want to
351 treat the 'a' as an *existential* type variable, in the sense described
352 by Note [Binding when looking up instances]. That is why isOverlappableTyVar
353 responds True to an InstSkol, which is the kind of skolem we use in
354 tcInstDecl2.
355
356
357 Note [Tricky type variable scoping]
358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
359 In our example
360 class C a where
361 op1, op2 :: Ix b => a -> b -> b
362 op2 = <dm-rhs>
363
364 instance C a => C [a]
365 {-# INLINE [2] op1 #-}
366 op1 = <rhs>
367
368 note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
369 in scope in <rhs>. In particular, we must make sure that 'b' is in
370 scope when typechecking <dm-rhs>. This is achieved by subFunTys,
371 which brings appropriate tyvars into scope. This happens for both
372 <dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
373 complained if 'b' is mentioned in <rhs>.
374
375
376
377 ************************************************************************
378 * *
379 \subsection{Extracting instance decls}
380 * *
381 ************************************************************************
382
383 Gather up the instance declarations from their various sources
384 -}
385
386 tcInstDecls1 -- Deal with both source-code and imported instance decls
387 :: [LInstDecl GhcRn] -- Source code instance decls
388 -> TcM (TcGblEnv, -- The full inst env
389 [InstInfo GhcRn], -- Source-code instance decls to process;
390 -- contains all dfuns for this module
391 [DerivInfo], -- From data family instances
392 ThBindEnv) -- TH binding levels
393
394 tcInstDecls1 inst_decls
395 = do { -- Do class and family instance declarations
396 ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
397
398 ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
399 fam_insts = concat fam_insts_s
400 local_infos = concat local_infos_s
401
402 ; (gbl_env, th_bndrs) <-
403 addClsInsts local_infos $
404 addFamInsts fam_insts
405
406 ; return ( gbl_env
407 , local_infos
408 , concat datafam_deriv_infos
409 , th_bndrs ) }
410
411 -- | Use DerivInfo for data family instances (produced by tcInstDecls1),
412 -- datatype declarations (TyClDecl), and standalone deriving declarations
413 -- (DerivDecl) to check and process all derived class instances.
414 tcInstDeclsDeriv
415 :: [DerivInfo]
416 -> [LDerivDecl GhcRn]
417 -> TcM (TcGblEnv, [InstInfo GhcRn], HsValBinds GhcRn)
418 tcInstDeclsDeriv deriv_infos derivds
419 = do th_stage <- getStage -- See Note [Deriving inside TH brackets]
420 if isBrackStage th_stage
421 then do { gbl_env <- getGblEnv
422 ; return (gbl_env, bagToList emptyBag, emptyValBindsOut) }
423 else do { (tcg_env, info_bag, valbinds) <- tcDeriving deriv_infos derivds
424 ; return (tcg_env, bagToList info_bag, valbinds) }
425
426 addClsInsts :: [InstInfo GhcRn] -> TcM a -> TcM a
427 addClsInsts infos thing_inside
428 = tcExtendLocalInstEnv (map iSpec infos) thing_inside
429
430 addFamInsts :: [FamInst] -> TcM (TcGblEnv, ThBindEnv)
431 -- Extend (a) the family instance envt
432 -- (b) the type envt with stuff from data type decls
433 addFamInsts fam_insts
434 = tcExtendLocalFamInstEnv fam_insts $
435 tcExtendGlobalEnv axioms $
436 do { traceTc "addFamInsts" (pprFamInsts fam_insts)
437 ; (gbl_env, th_bndrs) <- addTyConsToGblEnv data_rep_tycons
438 -- Does not add its axiom; that comes
439 -- from adding the 'axioms' above
440 ; return (gbl_env, th_bndrs)
441 }
442 where
443 axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
444 data_rep_tycons = famInstsRepTyCons fam_insts
445 -- The representation tycons for 'data instances' declarations
446
447 {-
448 Note [Deriving inside TH brackets]
449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
450 Given a declaration bracket
451 [d| data T = A | B deriving( Show ) |]
452
453 there is really no point in generating the derived code for deriving(
454 Show) and then type-checking it. This will happen at the call site
455 anyway, and the type check should never fail! Moreover (#6005)
456 the scoping of the generated code inside the bracket does not seem to
457 work out.
458
459 The easy solution is simply not to generate the derived instances at
460 all. (A less brutal solution would be to generate them with no
461 bindings.) This will become moot when we shift to the new TH plan, so
462 the brutal solution will do.
463 -}
464
465 tcLocalInstDecl :: LInstDecl GhcRn
466 -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
467 -- A source-file instance declaration
468 -- Type-check all the stuff before the "where"
469 --
470 -- We check for respectable instance type, and context
471 tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
472 = do { fam_inst <- tcTyFamInstDecl NotAssociated (L loc decl)
473 ; return ([], [fam_inst], []) }
474
475 tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
476 = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl NotAssociated emptyVarEnv (L loc decl)
477 ; return ([], [fam_inst], maybeToList m_deriv_info) }
478
479 tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
480 = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
481 ; return (insts, fam_insts, deriv_infos) }
482
483 tcClsInstDecl :: LClsInstDecl GhcRn
484 -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
485 -- The returned DerivInfos are for any associated data families
486 tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
487 , cid_sigs = uprags, cid_tyfam_insts = ats
488 , cid_overlap_mode = overlap_mode
489 , cid_datafam_insts = adts }))
490 = setSrcSpanA loc $
491 addErrCtxt (instDeclCtxt1 hs_ty) $
492 do { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
493 ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
494 -- NB: tcHsClsInstType does checkValidInstance
495
496 ; (subst, skol_tvs) <- tcInstSkolTyVars tyvars
497 ; let tv_skol_prs = [ (tyVarName tv, skol_tv)
498 | (tv, skol_tv) <- tyvars `zip` skol_tvs ]
499 -- Map from the skolemized Names to the original Names.
500 -- See Note [Associated data family instances and di_scoped_tvs].
501 tv_skol_env = mkVarEnv $ map swap tv_skol_prs
502 n_inferred = countWhile ((== Inferred) . binderArgFlag) $
503 fst $ splitForAllTyCoVarBinders dfun_ty
504 visible_skol_tvs = drop n_inferred skol_tvs
505
506 ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs)
507
508 -- Next, process any associated types.
509 ; (datafam_stuff, tyfam_insts)
510 <- tcExtendNameTyVarEnv tv_skol_prs $
511 do { let mini_env = mkVarEnv (classTyVars clas `zip` substTys subst inst_tys)
512 mini_subst = mkTvSubst (mkInScopeSet (mkVarSet skol_tvs)) mini_env
513 mb_info = InClsInst { ai_class = clas
514 , ai_tyvars = visible_skol_tvs
515 , ai_inst_env = mini_env }
516 ; df_stuff <- mapAndRecoverM (tcDataFamInstDecl mb_info tv_skol_env) adts
517 ; tf_insts1 <- mapAndRecoverM (tcTyFamInstDecl mb_info) ats
518
519 -- Check for missing associated types and build them
520 -- from their defaults (if available)
521 ; is_boot <- tcIsHsBootOrSig
522 ; let atItems = classATItems clas
523 ; tf_insts2 <- mapM (tcATDefault (locA loc) mini_subst defined_ats)
524 (if is_boot then [] else atItems)
525 -- Don't default type family instances, but rather omit, in hsig/hs-boot.
526 -- Since hsig/hs-boot files are essentially large binders we want omission
527 -- of the definition to result in no restriction, rather than for example
528 -- attempting to "pattern match" with the invisible defaults and generate
529 -- equalities. Without further handling, this would just result in a panic
530 -- anyway.
531 -- See https://github.com/ghc-proposals/ghc-proposals/pull/320 for
532 -- additional discussion.
533 ; return (df_stuff, tf_insts1 ++ concat tf_insts2) }
534
535
536 -- Finally, construct the Core representation of the instance.
537 -- (This no longer includes the associated types.)
538 ; dfun_name <- newDFunName clas inst_tys (getLocA hs_ty)
539 -- Dfun location is that of instance *header*
540
541 ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name
542 tyvars theta clas inst_tys
543
544 ; let inst_binds = InstBindings
545 { ib_binds = binds
546 , ib_tyvars = map Var.varName tyvars -- Scope over bindings
547 , ib_pragmas = uprags
548 , ib_extensions = []
549 , ib_derived = False }
550 inst_info = InstInfo { iSpec = ispec, iBinds = inst_binds }
551
552 (datafam_insts, m_deriv_infos) = unzip datafam_stuff
553 deriv_infos = catMaybes m_deriv_infos
554 all_insts = tyfam_insts ++ datafam_insts
555
556 -- In hs-boot files there should be no bindings
557 ; let no_binds = isEmptyLHsBinds binds && null uprags
558 ; is_boot <- tcIsHsBootOrSig
559 ; failIfTc (is_boot && not no_binds) TcRnIllegalHsBootFileDecl
560
561 ; return ( [inst_info], all_insts, deriv_infos ) }
562 where
563 defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
564 `unionNameSet`
565 mkNameSet (map (unLoc . feqn_tycon
566 . dfid_eqn
567 . unLoc) adts)
568
569 {-
570 ************************************************************************
571 * *
572 Type family instances
573 * *
574 ************************************************************************
575
576 Family instances are somewhat of a hybrid. They are processed together with
577 class instance heads, but can contain data constructors and hence they share a
578 lot of kinding and type checking code with ordinary algebraic data types (and
579 GADTs).
580 -}
581
582 tcTyFamInstDecl :: AssocInstInfo
583 -> LTyFamInstDecl GhcRn -> TcM FamInst
584 -- "type instance"
585 -- See Note [Associated type instances]
586 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
587 = setSrcSpanA loc $
588 tcAddTyFamInstCtxt decl $
589 do { let fam_lname = feqn_tycon eqn
590 ; fam_tc <- tcLookupLocatedTyCon fam_lname
591 ; tcFamInstDeclChecks mb_clsinfo fam_tc
592
593 -- (0) Check it's an open type family
594 ; checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
595 ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
596
597 -- (1) do the work of verifying the synonym group
598 -- For some reason we don't have a location for the equation
599 -- itself, so we make do with the location of family name
600 ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo
601 (L (na2la $ getLoc fam_lname) eqn)
602
603 -- (2) check for validity
604 ; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch
605 ; checkValidCoAxBranch fam_tc co_ax_branch
606
607 -- (3) construct coercion axiom
608 ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
609 ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
610 ; newFamInst SynFamilyInst axiom }
611
612
613 ---------------------
614 tcFamInstDeclChecks :: AssocInstInfo -> TyCon -> TcM ()
615 -- Used for both type and data families
616 tcFamInstDeclChecks mb_clsinfo fam_tc
617 = do { -- Type family instances require -XTypeFamilies
618 -- and can't (currently) be in an hs-boot file
619 ; traceTc "tcFamInstDecl" (ppr fam_tc)
620 ; type_families <- xoptM LangExt.TypeFamilies
621 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
622 ; checkTc type_families $ badFamInstDecl fam_tc
623 ; checkTc (not is_boot) $ badBootFamInstDeclErr
624
625 -- Check that it is a family TyCon, and that
626 -- oplevel type instances are not for associated types.
627 ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
628
629 ; when (isNotAssociated mb_clsinfo && -- Not in a class decl
630 isTyConAssoc fam_tc) -- but an associated type
631 (addErr $ assocInClassErr fam_tc)
632 }
633
634 {- Note [Associated type instances]
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636 We allow this:
637 class C a where
638 type T x a
639 instance C Int where
640 type T (S y) Int = y
641 type T Z Int = Char
642
643 Note that
644 a) The variable 'x' is not bound by the class decl
645 b) 'x' is instantiated to a non-type-variable in the instance
646 c) There are several type instance decls for T in the instance
647
648 All this is fine. Of course, you can't give any *more* instances
649 for (T ty Int) elsewhere, because it's an *associated* type.
650
651
652 ************************************************************************
653 * *
654 Data family instances
655 * *
656 ************************************************************************
657
658 For some reason data family instances are a lot more complicated
659 than type family instances
660 -}
661
662 tcDataFamInstDecl ::
663 AssocInstInfo
664 -> TyVarEnv Name -- If this is an associated data family instance, maps the
665 -- parent class's skolemized type variables to their
666 -- original Names. If this is a non-associated instance,
667 -- this will be empty.
668 -- See Note [Associated data family instances and di_scoped_tvs].
669 -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
670 -- "newtype instance" and "data instance"
671 tcDataFamInstDecl mb_clsinfo tv_skol_env
672 (L loc decl@(DataFamInstDecl { dfid_eqn =
673 FamEqn { feqn_bndrs = outer_bndrs
674 , feqn_pats = hs_pats
675 , feqn_tycon = lfam_name@(L _ fam_name)
676 , feqn_fixity = fixity
677 , feqn_rhs = HsDataDefn { dd_ND = new_or_data
678 , dd_cType = cType
679 , dd_ctxt = hs_ctxt
680 , dd_cons = hs_cons
681 , dd_kindSig = m_ksig
682 , dd_derivs = derivs } }}))
683 = setSrcSpanA loc $
684 tcAddDataFamInstCtxt decl $
685 do { fam_tc <- tcLookupLocatedTyCon lfam_name
686
687 ; tcFamInstDeclChecks mb_clsinfo fam_tc
688
689 -- Check that the family declaration is for the right kind
690 ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
691 ; gadt_syntax <- dataDeclChecks fam_name new_or_data hs_ctxt hs_cons
692 -- Do /not/ check that the number of patterns = tyConArity fam_tc
693 -- See [Arity of data families] in GHC.Core.FamInstEnv
694 ; (qtvs, pats, res_kind, stupid_theta)
695 <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
696 hs_ctxt hs_pats m_ksig new_or_data
697
698 -- Eta-reduce the axiom if possible
699 -- Quite tricky: see Note [Implementing eta reduction for data families]
700 ; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
701 eta_tvs = map binderVar eta_tcbs
702 post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
703
704 full_tcbs = mkTyConBindersPreferAnon post_eta_qtvs
705 (tyCoVarsOfType (mkSpecForAllTys eta_tvs res_kind))
706 ++ eta_tcbs
707 -- Put the eta-removed tyvars at the end
708 -- Remember, qtvs is in arbitrary order, except kind vars are
709 -- first, so there is no reason to suppose that the eta_tvs
710 -- (obtained from the pats) are at the end (#11148)
711
712 -- Eta-expand the representation tycon until it has result
713 -- kind `TYPE r`, for some `r`. If UnliftedNewtypes is not enabled, we
714 -- go one step further and ensure that it has kind `TYPE 'LiftedRep`.
715 --
716 -- See also Note [Arity of data families] in GHC.Core.FamInstEnv
717 -- NB: we can do this after eta-reducing the axiom, because if
718 -- we did it before the "extra" tvs from etaExpandAlgTyCon
719 -- would always be eta-reduced
720 --
721 ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
722
723 -- Check the result kind; it may come from a user-written signature.
724 -- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a)
725 ; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
726 all_pats = pats `chkAppend` extra_pats
727 orig_res_ty = mkTyConApp fam_tc all_pats
728 ty_binders = full_tcbs `chkAppend` extra_tcbs
729
730 ; traceTc "tcDataFamInstDecl" $
731 vcat [ text "Fam tycon:" <+> ppr fam_tc
732 , text "Pats:" <+> ppr pats
733 , text "visibilities:" <+> ppr (tcbVisibilities fam_tc pats)
734 , text "all_pats:" <+> ppr all_pats
735 , text "ty_binders" <+> ppr ty_binders
736 , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
737 , text "res_kind:" <+> ppr res_kind
738 , text "final_res_kind:" <+> ppr final_res_kind
739 , text "eta_pats" <+> ppr eta_pats
740 , text "eta_tcbs" <+> ppr eta_tcbs ]
741
742 ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
743 do { data_cons <- tcExtendTyVarEnv qtvs $
744 -- For H98 decls, the tyvars scope
745 -- over the data constructors
746 tcConDecls new_or_data (DDataInstance orig_res_ty)
747 rec_rep_tc ty_binders final_res_kind
748 hs_cons
749
750 ; rep_tc_name <- newFamInstTyConName lfam_name pats
751 ; axiom_name <- newFamInstAxiomName lfam_name [pats]
752 ; tc_rhs <- case new_or_data of
753 DataType -> return $
754 mkLevPolyDataTyConRhs
755 (isFixedRuntimeRepKind final_res_kind)
756 data_cons
757 NewType -> assert (not (null data_cons)) $
758 mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
759
760 ; let ax_rhs = mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs)
761 axiom = mkSingleCoAxiom Representational axiom_name
762 post_eta_qtvs eta_tvs [] fam_tc eta_pats ax_rhs
763 parent = DataFamInstTyCon axiom fam_tc all_pats
764
765 -- NB: Use the full ty_binders from the pats. See bullet toward
766 -- the end of Note [Data type families] in GHC.Core.TyCon
767 rep_tc = mkAlgTyCon rep_tc_name
768 ty_binders final_res_kind
769 (map (const Nominal) ty_binders)
770 (fmap unLoc cType) stupid_theta
771 tc_rhs parent
772 gadt_syntax
773 -- We always assume that indexed types are recursive. Why?
774 -- (1) Due to their open nature, we can never be sure that a
775 -- further instance might not introduce a new recursive
776 -- dependency. (2) They are always valid loop breakers as
777 -- they involve a coercion.
778 ; return (rep_tc, axiom) }
779
780 -- Remember to check validity; no recursion to worry about here
781 -- Check that left-hand sides are ok (mono-types, no type families,
782 -- consistent instantiations, etc)
783 ; let ax_branch = coAxiomSingleBranch axiom
784 ; checkConsistentFamInst mb_clsinfo fam_tc ax_branch
785 ; checkValidCoAxBranch fam_tc ax_branch
786 ; checkValidTyCon rep_tc
787
788 ; let scoped_tvs = map mk_deriv_info_scoped_tv_pr (tyConTyVars rep_tc)
789 m_deriv_info = case derivs of
790 [] -> Nothing
791 preds ->
792 Just $ DerivInfo { di_rep_tc = rep_tc
793 , di_scoped_tvs = scoped_tvs
794 , di_clauses = preds
795 , di_ctxt = tcMkDataFamInstCtxt decl }
796
797 ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
798 ; return (fam_inst, m_deriv_info) }
799 where
800 eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
801 -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
802 -- Splits the incoming patterns into two: the [TyVar]
803 -- are the patterns that can be eta-reduced away.
804 -- e.g. T [a] Int a d c ==> (T [a] Int a, [d,c])
805 --
806 -- NB: quadratic algorithm, but types are small here
807 eta_reduce fam_tc pats
808 = go (reverse (zip3 pats fvs_s vis_s)) []
809 where
810 vis_s :: [TyConBndrVis]
811 vis_s = tcbVisibilities fam_tc pats
812
813 fvs_s :: [TyCoVarSet] -- 1-1 correspondence with pats
814 -- Each elt is the free vars of all /earlier/ pats
815 (_, fvs_s) = mapAccumL add_fvs emptyVarSet pats
816 add_fvs fvs pat = (fvs `unionVarSet` tyCoVarsOfType pat, fvs)
817
818 go ((pat, fvs_to_the_left, tcb_vis):pats) etad_tvs
819 | Just tv <- getTyVar_maybe pat
820 , not (tv `elemVarSet` fvs_to_the_left)
821 = go pats (Bndr tv tcb_vis : etad_tvs)
822 go pats etad_tvs = (reverse (map fstOf3 pats), etad_tvs)
823
824 -- Create a Name-TyVar mapping to bring into scope when typechecking any
825 -- deriving clauses this data family instance may have.
826 -- See Note [Associated data family instances and di_scoped_tvs].
827 mk_deriv_info_scoped_tv_pr :: TyVar -> (Name, TyVar)
828 mk_deriv_info_scoped_tv_pr tv =
829 let n = lookupWithDefaultVarEnv tv_skol_env (tyVarName tv) tv
830 in (n, tv)
831
832 {-
833 Note [Associated data family instances and di_scoped_tvs]
834 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
835 Some care is required to implement `deriving` correctly for associated data
836 family instances. Consider this example from #18055:
837
838 class C a where
839 data D a
840
841 class X a b
842
843 instance C (Maybe a) where
844 data D (Maybe a) deriving (X a)
845
846 When typechecking the `X a` in `deriving (X a)`, we must ensure that the `a`
847 from the instance header is brought into scope. This is the role of
848 di_scoped_tvs, which maps from the original, renamed `a` to the skolemized,
849 typechecked `a`. When typechecking the `deriving` clause, this mapping will be
850 consulted when looking up the `a` in `X a`.
851
852 A naïve attempt at creating the di_scoped_tvs is to simply reuse the
853 tyConTyVars of the representation TyCon for `data D (Maybe a)`. This is only
854 half correct, however. We do want the typechecked `a`'s Name in the /range/
855 of the mapping, but we do not want it in the /domain/ of the mapping.
856 To ensure that the original `a`'s Name ends up in the domain, we consult a
857 TyVarEnv (passed as an argument to tcDataFamInstDecl) that maps from the
858 typechecked `a`'s Name to the original `a`'s Name. In the even that
859 tcDataFamInstDecl is processing a non-associated data family instance, this
860 TyVarEnv will simply be empty, and there is nothing to worry about.
861 -}
862
863 -----------------------
864 tcDataFamInstHeader
865 :: AssocInstInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
866 -> LexicalFixity -> Maybe (LHsContext GhcRn)
867 -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn)
868 -> NewOrData
869 -> TcM ([TyVar], [Type], Kind, ThetaType)
870 -- The "header" of a data family instance is the part other than
871 -- the data constructors themselves
872 -- e.g. data instance D [a] :: * -> * where ...
873 -- Here the "header" is the bit before the "where"
874 tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
875 hs_ctxt hs_pats m_ksig new_or_data
876 = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
877 ; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
878 <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
879 bindOuterFamEqnTKBndrs outer_bndrs $
880 do { stupid_theta <- tcHsContext hs_ctxt
881 ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
882 ; (lhs_applied_ty, lhs_applied_kind)
883 <- tcInstInvisibleTyBinders lhs_ty lhs_kind
884 -- See Note [Data family/instance return kinds]
885 -- in GHC.Tc.TyCl point (DF3)
886
887 -- Ensure that the instance is consistent
888 -- with its parent class
889 ; addConsistencyConstraints mb_clsinfo lhs_ty
890
891 -- Add constraints from the result signature
892 ; res_kind <- tc_kind_sig m_ksig
893
894 -- Do not add constraints from the data constructors
895 -- See Note [Kind inference for data family instances]
896
897 -- Check that the result kind of the TyCon applied to its args
898 -- is compatible with the explicit signature (or Type, if there
899 -- is none)
900 ; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
901 ; _ <- unifyKind (Just (ppr hs_lhs)) lhs_applied_kind res_kind
902
903 ; traceTc "tcDataFamInstHeader" $
904 vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ]
905 ; return ( stupid_theta
906 , lhs_applied_ty
907 , lhs_applied_kind
908 , res_kind ) }
909
910 -- This code (and the stuff immediately above) is very similar
911 -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the
912 -- common code; but for the moment I concluded that it's
913 -- clearer to duplicate it. Still, if you fix a bug here,
914 -- check there too!
915
916 -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
917 ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
918 ; qtvs <- quantifyTyVars noVarsOfKindDefault dvs
919 ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
920
921 -- Zonk the patterns etc into the Type world
922 ; ze <- mkEmptyZonkEnv NoFlexi
923 ; (ze, qtvs) <- zonkTyBndrsX ze qtvs
924 ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
925 ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
926 ; master_res_kind <- zonkTcTypeToTypeX ze master_res_kind
927 ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
928
929 -- We check that res_kind is OK with checkDataKindSig in
930 -- tcDataFamInstDecl, after eta-expansion. We need to check that
931 -- it's ok because res_kind can come from a user-written kind signature.
932 -- See Note [Datatype return kinds], point (4a)
933
934 ; checkDataKindSig (DataInstanceSort new_or_data) master_res_kind
935 ; checkDataKindSig (DataInstanceSort new_or_data) instance_res_kind
936
937 -- Check that type patterns match the class instance head
938 -- The call to splitTyConApp_maybe here is just an inlining of
939 -- the body of unravelFamInstPats.
940 ; pats <- case splitTyConApp_maybe lhs_ty of
941 Just (_, pats) -> pure pats
942 Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
943
944 ; return (qtvs, pats, master_res_kind, stupid_theta) }
945 where
946 fam_name = tyConName fam_tc
947 data_ctxt = DataKindCtxt fam_name
948
949 -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2),
950 -- and Note [Implementation of UnliftedDatatypes].
951 tc_kind_sig Nothing
952 = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
953 ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes
954 ; case new_or_data of
955 NewType | unlifted_newtypes -> newOpenTypeKind
956 DataType | unlifted_datatypes -> newOpenTypeKind
957 _ -> pure liftedTypeKind
958 }
959
960 -- See Note [Result kind signature for a data family instance]
961 tc_kind_sig (Just hs_kind)
962 = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
963 ; lvl <- getTcLevel
964 ; let (tvs, inner_kind) = tcSplitForAllInvisTyVars sig_kind
965 ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
966 -- Perhaps surprisingly, we don't need the skolemised tvs themselves
967 ; return (substTy subst inner_kind) }
968
969 {- Note [Result kind signature for a data family instance]
970 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
971 The expected type might have a forall at the type. Normally, we
972 can't skolemise in kinds because we don't have type-level lambda.
973 But here, we're at the top-level of an instance declaration, so
974 we actually have a place to put the regeneralised variables.
975 Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcSkolemise
976 Examples in indexed-types/should_compile/T12369
977
978 Note [Implementing eta reduction for data families]
979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
980 Consider
981 data D :: * -> * -> * -> * -> *
982
983 data instance D [(a,b)] p q :: * -> * where
984 D1 :: blah1
985 D2 :: blah2
986
987 Then we'll generate a representation data type
988 data Drep a b p q z where
989 D1 :: blah1
990 D2 :: blah2
991
992 and an axiom to connect them
993 axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z
994
995 except that we'll eta-reduce the axiom to
996 axiom AxDrep forall a b. D [(a,b]] = Drep a b
997
998 This is described at some length in Note [Eta reduction for data families]
999 in GHC.Core.Coercion.Axiom. There are several fiddly subtleties lurking here,
1000 however, so this Note aims to describe these subtleties:
1001
1002 * The representation tycon Drep is parameterised over the free
1003 variables of the pattern, in no particular order. So there is no
1004 guarantee that 'p' and 'q' will come last in Drep's parameters, and
1005 in the right order. So, if the /patterns/ of the family instance
1006 are eta-reducible, we re-order Drep's parameters to put the
1007 eta-reduced type variables last.
1008
1009 * Although we eta-reduce the axiom, we eta-/expand/ the representation
1010 tycon Drep. The kind of D says it takes four arguments, but the
1011 data instance header only supplies three. But the AlgTyCon for Drep
1012 itself must have enough TyConBinders so that its result kind is Type.
1013 So, with etaExpandAlgTyCon we make up some extra TyConBinders.
1014 See point (3) in Note [Datatype return kinds] in GHC.Tc.TyCl.
1015
1016 * The result kind in the instance might be a polykind, like this:
1017 data family DP a :: forall k. k -> *
1018 data instance DP [b] :: forall k1 k2. (k1,k2) -> *
1019
1020 So in type-checking the LHS (DP Int) we need to check that it is
1021 more polymorphic than the signature. To do that we must skolemise
1022 the signature and instantiate the call of DP. So we end up with
1023 data instance DP [b] @(k1,k2) (z :: (k1,k2)) where
1024
1025 Note that we must parameterise the representation tycon DPrep over
1026 'k1' and 'k2', as well as 'b'.
1027
1028 The skolemise bit is done in tc_kind_sig, while the instantiate bit
1029 is done by tcFamTyPats.
1030
1031 * Very fiddly point. When we eta-reduce to
1032 axiom AxDrep forall a b. D [(a,b]] = Drep a b
1033
1034 we want the kind of (D [(a,b)]) to be the same as the kind of
1035 (Drep a b). This ensures that applying the axiom doesn't change the
1036 kind. Why is that hard? Because the kind of (Drep a b) depends on
1037 the TyConBndrVis on Drep's arguments. In particular do we have
1038 (forall (k::*). blah) or (* -> blah)?
1039
1040 We must match whatever D does! In #15817 we had
1041 data family X a :: forall k. * -> * -- Note: a forall that is not used
1042 data instance X Int b = MkX
1043
1044 So the data instance is really
1045 data istance X Int @k b = MkX
1046
1047 The axiom will look like
1048 axiom X Int = Xrep
1049
1050 and it's important that XRep :: forall k * -> *, following X.
1051
1052 To achieve this we get the TyConBndrVis flags from tcbVisibilities,
1053 and use those flags for any eta-reduced arguments. Sigh.
1054
1055 * The final turn of the knife is that tcbVisibilities is itself
1056 tricky to sort out. Consider
1057 data family D k :: k
1058 Then consider D (forall k2. k2 -> k2) Type Type
1059 The visibility flags on an application of D may affected by the arguments
1060 themselves. Heavy sigh. But not truly hard; that's what tcbVisibilities
1061 does.
1062
1063 * Happily, we don't need to worry about the possibility of
1064 building an inhomogeneous axiom, described in GHC.Tc.TyCl.Build
1065 Note [Newtype eta and homogeneous axioms]. For example
1066 type F :: Type -> forall (b :: Type) -> Type
1067 data family F a b
1068 newtype instance F Int b = MkF (Proxy b)
1069 we get a newtype, and a eta-reduced axiom connecting the data family
1070 with the newtype:
1071 type R:FIntb :: forall (b :: Type) -> Type
1072 newtype R:FIntb b = MkF (Proxy b)
1073 axiom Foo.D:R:FIntb0 :: F Int = Foo.R:FIntb
1074 Now the subtleties of Note [Newtype eta and homogeneous axioms] are
1075 dealt with by the newtype (via mkNewTyConRhs called in tcDataFamInstDecl)
1076 while the axiom connecting F Int ~ R:FIntb is eta-reduced, but the
1077 quantifer 'b' is derived from the original data family F, and so the
1078 kinds will always match.
1079
1080 Note [Kind inference for data family instances]
1081 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1082 Consider this GADT-style data type declaration, where I have used
1083 fresh variables in the data constructor's type, to stress that c,d are
1084 quite distinct from a,b.
1085 data T a b where
1086 MkT :: forall c d. c d -> T c d
1087
1088 Following Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
1089 to infer T's kind, we initially give T :: kappa, a monomorpic kind,
1090 gather constraints from the header and data constructors, and conclude
1091 T :: (kappa1 -> type) -> kappa1 -> Type
1092 Then we generalise, giving
1093 T :: forall k. (k->Type) -> k -> Type
1094
1095 Now what about a data /instance/ decl
1096 data family T :: forall k. (k->Type) -> k -> Type
1097
1098 data instance T p Int where ...
1099
1100 No doubt here! The poly-kinded T is instantiated with k=Type, so the
1101 header really looks like
1102 data instance T @Type (p :: Type->Type) Int where ...
1103
1104 But what about this?
1105 data instance T p q where
1106 MkT :: forall r. r Int -> T r Int
1107
1108 So what kind do 'p' and 'q' have? No clues from the header, but from
1109 the data constructor we can clearly see that (r :: Type->Type). Does
1110 that mean that the the /entire data instance/ is instantiated at Type,
1111 like this?
1112 data instance T @Type (p :: Type->Type) (q :: Type) where
1113 ...
1114
1115 Not at all! This is a /GADT/-style decl, so the kind argument might
1116 be specialised in this particular data constructor, thus:
1117 data instance T @k (p :: k->Type) (q :: k) where
1118 MkT :: forall (r :: Type -> Type).
1119 r Int -> T @Type r Int
1120 (and perhaps specialised differently in some other data
1121 constructor MkT2).
1122
1123 The key difference in this case and 'data T' at the top of this Note
1124 is that we have no known kind for 'data T'. We thus forbid different
1125 specialisations of T in its constructors, in an attempt to avoid
1126 inferring polymorphic recursion. In data family T, however, there is
1127 no problem with polymorphic recursion: we already /fully know/ T's
1128 kind -- that came from the family declaration, and is not influenced
1129 by the data instances -- and hence we /can/ specialise T's kind
1130 differently in different GADT data constructors.
1131
1132 SHORT SUMMARY: in a data instance decl, it's not clear whether kind
1133 constraints arising from the data constructors should be considered
1134 local to the (GADT) data /constructor/ or should apply to the entire
1135 data instance.
1136
1137 DESIGN CHOICE: in data/newtype family instance declarations, we ignore
1138 the /data constructor/ declarations altogether, looking only at the
1139 data instance /header/.
1140
1141 Observations:
1142 * This choice is simple to describe, as well as simple to implement.
1143 For a data/newtype instance decl, the instance kinds are influenced
1144 /only/ by the header.
1145
1146 * We could treat Haskell-98 style data-instance decls differently, by
1147 taking the data constructors into account, since there are no GADT
1148 issues. But we don't, for simplicity, and because it means you can
1149 understand the data type instance by looking only at the header.
1150
1151 * Newtypes can be declared in GADT syntax, but they can't do GADT-style
1152 specialisation, so like Haskell-98 definitions we could take the
1153 data constructors into account. Again we don't, for the same reason.
1154
1155 So for now at least, we keep the simplest choice. See #18891 and !4419
1156 for more discussion of this issue.
1157
1158 Kind inference for data types (Xie et al) https://arxiv.org/abs/1911.06153
1159 takes a slightly different approach.
1160 -}
1161
1162
1163 {- *********************************************************************
1164 * *
1165 Class instance declarations, pass 2
1166 * *
1167 ********************************************************************* -}
1168
1169 tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn] -> ClassScopedTVEnv
1170 -> TcM (LHsBinds GhcTc)
1171 -- (a) From each class declaration,
1172 -- generate any default-method bindings
1173 -- (b) From each instance decl
1174 -- generate the dfun binding
1175
1176 tcInstDecls2 tycl_decls inst_decls class_scoped_tv_env
1177 = do { -- (a) Default methods from class decls
1178 let class_decls = filter (isClassDecl . unLoc) tycl_decls
1179 ; dm_binds_s <- mapM (tcClassDecl2 class_scoped_tv_env) class_decls
1180 ; let dm_binds = unionManyBags dm_binds_s
1181
1182 -- (b) instance declarations
1183 ; let dm_ids = collectHsBindsBinders CollNoDictBinders dm_binds
1184 -- Add the default method Ids (again)
1185 -- (they were already added in GHC.Tc.TyCl.Utils.tcAddImplicits)
1186 -- See Note [Default methods in the type environment]
1187 ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
1188 mapM tcInstDecl2 inst_decls
1189
1190 -- Done
1191 ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
1192
1193 {- Note [Default methods in the type environment]
1194 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1195 The default method Ids are already in the type environment (see Note
1196 [Default method Ids and Template Haskell] in TcTyDcls), BUT they
1197 don't have their InlinePragmas yet. Usually that would not matter,
1198 because the simplifier propagates information from binding site to
1199 use. But, unusually, when compiling instance decls we *copy* the
1200 INLINE pragma from the default method to the method for that
1201 particular operation (see Note [INLINE and default methods] below).
1202
1203 So right here in tcInstDecls2 we must re-extend the type envt with
1204 the default method Ids replete with their INLINE pragmas. Urk.
1205 -}
1206
1207 tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
1208 -- Returns a binding for the dfun
1209 tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
1210 = recoverM (return emptyLHsBinds) $
1211 setSrcSpan loc $
1212 addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
1213 do { -- Instantiate the instance decl with skolem constants
1214 ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
1215 ; dfun_ev_vars <- newEvVars dfun_theta
1216 -- We instantiate the dfun_id with superSkolems.
1217 -- See Note [Subtle interaction of recursion and overlap]
1218 -- and Note [Binding when looking up instances]
1219
1220 ; let (clas, inst_tys) = tcSplitDFunHead inst_head
1221 (class_tyvars, sc_theta, _, op_items) = classBigSig clas
1222 sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
1223
1224 ; traceTc "tcInstDecl2" (vcat [ppr inst_tyvars, ppr inst_tys, ppr dfun_theta, ppr sc_theta'])
1225
1226 -- Deal with 'SPECIALISE instance' pragmas
1227 -- See Note [SPECIALISE instance pragmas]
1228 ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
1229
1230 -- Typecheck superclasses and methods
1231 -- See Note [Typechecking plan for instance declarations]
1232 ; dfun_ev_binds_var <- newTcEvBinds
1233 ; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
1234 ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
1235 <- pushTcLevelM $
1236 do { (sc_ids, sc_binds, sc_implics)
1237 <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
1238 inst_tys dfun_ev_binds
1239 sc_theta'
1240
1241 -- Typecheck the methods
1242 ; (meth_ids, meth_binds, meth_implics)
1243 <- tcMethods dfun_id clas inst_tyvars dfun_ev_vars
1244 inst_tys dfun_ev_binds spec_inst_info
1245 op_items ibinds
1246
1247 ; return ( sc_ids ++ meth_ids
1248 , sc_binds `unionBags` meth_binds
1249 , sc_implics `unionBags` meth_implics ) }
1250
1251 ; imp <- newImplication
1252 ; emitImplication $
1253 imp { ic_tclvl = tclvl
1254 , ic_skols = inst_tyvars
1255 , ic_given = dfun_ev_vars
1256 , ic_wanted = mkImplicWC sc_meth_implics
1257 , ic_binds = dfun_ev_binds_var
1258 , ic_info = InstSkol }
1259
1260 -- Create the result bindings
1261 ; self_dict <- newDict clas inst_tys
1262 ; let class_tc = classTyCon clas
1263 loc' = noAnnSrcSpan loc
1264 [dict_constr] = tyConDataCons class_tc
1265 dict_bind = mkVarBind self_dict (L loc' con_app_args)
1266
1267 -- We don't produce a binding for the dict_constr; instead we
1268 -- rely on the simplifier to unfold this saturated application
1269 -- We do this rather than generate an HsCon directly, because
1270 -- it means that the special cases (e.g. dictionary with only one
1271 -- member) are dealt with by the common MkId.mkDataConWrapId
1272 -- code rather than needing to be repeated here.
1273 -- con_app_tys = MkD ty1 ty2
1274 -- con_app_scs = MkD ty1 ty2 sc1 sc2
1275 -- con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
1276 con_app_tys = mkHsWrap (mkWpTyApps inst_tys) $
1277 mkConLikeTc (RealDataCon dict_constr)
1278 -- NB: We *can* have covars in inst_tys, in the case of
1279 -- promoted GADT constructors.
1280
1281 con_app_args = foldl' app_to_meth con_app_tys sc_meth_ids
1282
1283 app_to_meth :: HsExpr GhcTc -> Id -> HsExpr GhcTc
1284 app_to_meth fun meth_id = HsApp noComments (L loc' fun)
1285 (L loc' (wrapId arg_wrapper meth_id))
1286
1287 inst_tv_tys = mkTyVarTys inst_tyvars
1288 arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
1289
1290 is_newtype = isNewTyCon class_tc
1291 dfun_id_w_prags = addDFunPrags dfun_id sc_meth_ids
1292 dfun_spec_prags
1293 | is_newtype = SpecPrags []
1294 | otherwise = SpecPrags spec_inst_prags
1295 -- Newtype dfuns just inline unconditionally,
1296 -- so don't attempt to specialise them
1297
1298 export = ABE { abe_ext = noExtField
1299 , abe_wrap = idHsWrapper
1300 , abe_poly = dfun_id_w_prags
1301 , abe_mono = self_dict
1302 , abe_prags = dfun_spec_prags }
1303 -- NB: see Note [SPECIALISE instance pragmas]
1304 main_bind = AbsBinds { abs_ext = noExtField
1305 , abs_tvs = inst_tyvars
1306 , abs_ev_vars = dfun_ev_vars
1307 , abs_exports = [export]
1308 , abs_ev_binds = []
1309 , abs_binds = unitBag dict_bind
1310 , abs_sig = True }
1311
1312 ; return (unitBag (L loc' main_bind)
1313 `unionBags` sc_meth_binds)
1314 }
1315 where
1316 dfun_id = instanceDFunId ispec
1317 loc = getSrcSpan dfun_id
1318
1319 addDFunPrags :: DFunId -> [Id] -> DFunId
1320 -- DFuns need a special Unfolding and InlinePrag
1321 -- See Note [ClassOp/DFun selection]
1322 -- and Note [Single-method classes]
1323 -- It's easiest to create those unfoldings right here, where
1324 -- have all the pieces in hand, even though we are messing with
1325 -- Core at this point, which the typechecker doesn't usually do
1326 -- However we take care to build the unfolding using the TyVars from
1327 -- the DFunId rather than from the skolem pieces that the typechecker
1328 -- is messing with.
1329 addDFunPrags dfun_id sc_meth_ids
1330 | is_newtype
1331 = dfun_id `setIdUnfolding` mkInlineUnfoldingWithArity 0 defaultSimpleOpts con_app
1332 `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
1333 | otherwise
1334 = dfun_id `setIdUnfolding` mkDFunUnfolding dfun_bndrs dict_con dict_args
1335 `setInlinePragma` dfunInlinePragma
1336 where
1337 con_app = mkLams dfun_bndrs $
1338 mkApps (Var (dataConWrapId dict_con)) dict_args
1339 -- This application will satisfy the Core invariants
1340 -- from Note [Representation polymorphism invariants] in GHC.Core,
1341 -- because typeclass method types are never unlifted.
1342 dict_args = map Type inst_tys ++
1343 [mkVarApps (Var id) dfun_bndrs | id <- sc_meth_ids]
1344
1345 (dfun_tvs, dfun_theta, clas, inst_tys) = tcSplitDFunTy (idType dfun_id)
1346 ev_ids = mkTemplateLocalsNum 1 dfun_theta
1347 dfun_bndrs = dfun_tvs ++ ev_ids
1348 clas_tc = classTyCon clas
1349 [dict_con] = tyConDataCons clas_tc
1350 is_newtype = isNewTyCon clas_tc
1351
1352 wrapId :: HsWrapper -> Id -> HsExpr GhcTc
1353 wrapId wrapper id = mkHsWrap wrapper (HsVar noExtField (noLocA id))
1354
1355 {- Note [Typechecking plan for instance declarations]
1356 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1357 For instance declarations we generate the following bindings and implication
1358 constraints. Example:
1359
1360 instance Ord a => Ord [a] where compare = <compare-rhs>
1361
1362 generates this:
1363
1364 Bindings:
1365 -- Method bindings
1366 $ccompare :: forall a. Ord a => a -> a -> Ordering
1367 $ccompare = /\a \(d:Ord a). let <meth-ev-binds> in ...
1368
1369 -- Superclass bindings
1370 $cp1Ord :: forall a. Ord a => Eq [a]
1371 $cp1Ord = /\a \(d:Ord a). let <sc-ev-binds>
1372 in dfEqList (dw :: Eq a)
1373
1374 Constraints:
1375 forall a. Ord a =>
1376 -- Method constraint
1377 (forall. (empty) => <constraints from compare-rhs>)
1378 -- Superclass constraint
1379 /\ (forall. (empty) => dw :: Eq a)
1380
1381 Notice that
1382
1383 * Per-meth/sc implication. There is one inner implication per
1384 superclass or method, with no skolem variables or givens. The only
1385 reason for this one is to gather the evidence bindings privately
1386 for this superclass or method. This implication is generated
1387 by checkInstConstraints.
1388
1389 * Overall instance implication. There is an overall enclosing
1390 implication for the whole instance declaration, with the expected
1391 skolems and givens. We need this to get the correct "redundant
1392 constraint" warnings, gathering all the uses from all the methods
1393 and superclasses. See GHC.Tc.Solver Note [Tracking redundant
1394 constraints]
1395
1396 * The given constraints in the outer implication may generate
1397 evidence, notably by superclass selection. Since the method and
1398 superclass bindings are top-level, we want that evidence copied
1399 into *every* method or superclass definition. (Some of it will
1400 be usused in some, but dead-code elimination will drop it.)
1401
1402 We achieve this by putting the evidence variable for the overall
1403 instance implication into the AbsBinds for each method/superclass.
1404 Hence the 'dfun_ev_binds' passed into tcMethods and tcSuperClasses.
1405 (And that in turn is why the abs_ev_binds field of AbBinds is a
1406 [TcEvBinds] rather than simply TcEvBinds.
1407
1408 This is a bit of a hack, but works very nicely in practice.
1409
1410 * Note that if a method has a locally-polymorphic binding, there will
1411 be yet another implication for that, generated by tcPolyCheck
1412 in tcMethodBody. E.g.
1413 class C a where
1414 foo :: forall b. Ord b => blah
1415
1416
1417 ************************************************************************
1418 * *
1419 Type-checking superclasses
1420 * *
1421 ************************************************************************
1422 -}
1423
1424 tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
1425 -> TcEvBinds
1426 -> TcThetaType
1427 -> TcM ([EvVar], LHsBinds GhcTc, Bag Implication)
1428 -- Make a new top-level function binding for each superclass,
1429 -- something like
1430 -- $Ordp1 :: forall a. Ord a => Eq [a]
1431 -- $Ordp1 = /\a \(d:Ord a). dfunEqList a (sc_sel d)
1432 --
1433 -- See Note [Recursive superclasses] for why this is so hard!
1434 -- In effect, we build a special-purpose solver for the first step
1435 -- of solving each superclass constraint
1436 tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
1437 = do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
1438 ; return (ids, listToBag binds, listToBag implics) }
1439 where
1440 loc = getSrcSpan dfun_id
1441 size = sizeTypes inst_tys
1442 tc_super (sc_pred, n)
1443 = do { (sc_implic, ev_binds_var, sc_ev_tm)
1444 <- checkInstConstraints $ emitWanted (ScOrigin size) sc_pred
1445
1446 ; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
1447 ; sc_ev_id <- newEvVar sc_pred
1448 ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
1449 ; let sc_top_ty = mkInfForAllTys tyvars $
1450 mkPhiTy (map idType dfun_evs) sc_pred
1451 sc_top_id = mkLocalId sc_top_name Many sc_top_ty
1452 export = ABE { abe_ext = noExtField
1453 , abe_wrap = idHsWrapper
1454 , abe_poly = sc_top_id
1455 , abe_mono = sc_ev_id
1456 , abe_prags = noSpecPrags }
1457 local_ev_binds = TcEvBinds ev_binds_var
1458 bind = AbsBinds { abs_ext = noExtField
1459 , abs_tvs = tyvars
1460 , abs_ev_vars = dfun_evs
1461 , abs_exports = [export]
1462 , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
1463 , abs_binds = emptyBag
1464 , abs_sig = False }
1465 ; return (sc_top_id, L (noAnnSrcSpan loc) bind, sc_implic) }
1466
1467 -------------------
1468 checkInstConstraints :: TcM result
1469 -> TcM (Implication, EvBindsVar, result)
1470 -- See Note [Typechecking plan for instance declarations]
1471 checkInstConstraints thing_inside
1472 = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints $
1473 thing_inside
1474
1475 ; ev_binds_var <- newTcEvBinds
1476 ; implic <- newImplication
1477 ; let implic' = implic { ic_tclvl = tclvl
1478 , ic_wanted = wanted
1479 , ic_binds = ev_binds_var
1480 , ic_info = InstSkol }
1481
1482 ; return (implic', ev_binds_var, result) }
1483
1484 {-
1485 Note [Recursive superclasses]
1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1487 See #3731, #4809, #5751, #5913, #6117, #6161, which all
1488 describe somewhat more complicated situations, but ones
1489 encountered in practice.
1490
1491 See also tests tcrun020, tcrun021, tcrun033, and #11427.
1492
1493 ----- THE PROBLEM --------
1494 The problem is that it is all too easy to create a class whose
1495 superclass is bottom when it should not be.
1496
1497 Consider the following (extreme) situation:
1498 class C a => D a where ...
1499 instance D [a] => D [a] where ... (dfunD)
1500 instance C [a] => C [a] where ... (dfunC)
1501 Although this looks wrong (assume D [a] to prove D [a]), it is only a
1502 more extreme case of what happens with recursive dictionaries, and it
1503 can, just about, make sense because the methods do some work before
1504 recursing.
1505
1506 To implement the dfunD we must generate code for the superclass C [a],
1507 which we had better not get by superclass selection from the supplied
1508 argument:
1509 dfunD :: forall a. D [a] -> D [a]
1510 dfunD = \d::D [a] -> MkD (scsel d) ..
1511
1512 Otherwise if we later encounter a situation where
1513 we have a [Wanted] dw::D [a] we might solve it thus:
1514 dw := dfunD dw
1515 Which is all fine except that now ** the superclass C is bottom **!
1516
1517 The instance we want is:
1518 dfunD :: forall a. D [a] -> D [a]
1519 dfunD = \d::D [a] -> MkD (dfunC (scsel d)) ...
1520
1521 ----- THE SOLUTION --------
1522 The basic solution is simple: be very careful about using superclass
1523 selection to generate a superclass witness in a dictionary function
1524 definition. More precisely:
1525
1526 Superclass Invariant: in every class dictionary,
1527 every superclass dictionary field
1528 is non-bottom
1529
1530 To achieve the Superclass Invariant, in a dfun definition we can
1531 generate a guaranteed-non-bottom superclass witness from:
1532 (sc1) one of the dictionary arguments itself (all non-bottom)
1533 (sc2) an immediate superclass of a smaller dictionary
1534 (sc3) a call of a dfun (always returns a dictionary constructor)
1535
1536 The tricky case is (sc2). We proceed by induction on the size of
1537 the (type of) the dictionary, defined by GHC.Tc.Validity.sizeTypes.
1538 Let's suppose we are building a dictionary of size 3, and
1539 suppose the Superclass Invariant holds of smaller dictionaries.
1540 Then if we have a smaller dictionary, its immediate superclasses
1541 will be non-bottom by induction.
1542
1543 What does "we have a smaller dictionary" mean? It might be
1544 one of the arguments of the instance, or one of its superclasses.
1545 Here is an example, taken from CmmExpr:
1546 class Ord r => UserOfRegs r a where ...
1547 (i1) instance UserOfRegs r a => UserOfRegs r (Maybe a) where
1548 (i2) instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
1549
1550 For (i1) we can get the (Ord r) superclass by selection from (UserOfRegs r a),
1551 since it is smaller than the thing we are building (UserOfRegs r (Maybe a).
1552
1553 But for (i2) that isn't the case, so we must add an explicit, and
1554 perhaps surprising, (Ord r) argument to the instance declaration.
1555
1556 Here's another example from #6161:
1557
1558 class Super a => Duper a where ...
1559 class Duper (Fam a) => Foo a where ...
1560 (i3) instance Foo a => Duper (Fam a) where ...
1561 (i4) instance Foo Float where ...
1562
1563 It would be horribly wrong to define
1564 dfDuperFam :: Foo a -> Duper (Fam a) -- from (i3)
1565 dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ...
1566
1567 dfFooFloat :: Foo Float -- from (i4)
1568 dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ...
1569
1570 Now the Super superclass of Duper is definitely bottom!
1571
1572 This won't happen because when processing (i3) we can use the
1573 superclasses of (Foo a), which is smaller, namely Duper (Fam a). But
1574 that is *not* smaller than the target so we can't take *its*
1575 superclasses. As a result the program is rightly rejected, unless you
1576 add (Super (Fam a)) to the context of (i3).
1577
1578 Note [Solving superclass constraints]
1579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1580 How do we ensure that every superclass witness is generated by
1581 one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses].
1582 Answer:
1583
1584 * Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
1585 where 'size' is the size of the instance declaration. e.g.
1586 class C a => D a where...
1587 instance blah => D [a] where ...
1588 The wanted superclass constraint for C [a] has origin
1589 ScOrigin size, where size = size( D [a] ).
1590
1591 * (sc1) When we rewrite such a wanted constraint, it retains its
1592 origin. But if we apply an instance declaration, we can set the
1593 origin to (ScOrigin infinity), thus lifting any restrictions by
1594 making prohibitedSuperClassSolve return False.
1595
1596 * (sc2) ScOrigin wanted constraints can't be solved from a
1597 superclass selection, except at a smaller type. This test is
1598 implemented by GHC.Tc.Solver.Interact.prohibitedSuperClassSolve
1599
1600 * The "given" constraints of an instance decl have CtOrigin
1601 GivenOrigin InstSkol.
1602
1603 * When we make a superclass selection from InstSkol we use
1604 a SkolemInfo of (InstSC size), where 'size' is the size of
1605 the constraint whose superclass we are taking. A similarly
1606 when taking the superclass of an InstSC. This is implemented
1607 in GHC.Tc.Solver.Canonical.newSCWorkFromFlavored
1608
1609 Note [Silent superclass arguments] (historical interest only)
1610 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1611 NB1: this note describes our *old* solution to the
1612 recursive-superclass problem. I'm keeping the Note
1613 for now, just as institutional memory.
1614 However, the code for silent superclass arguments
1615 was removed in late Dec 2014
1616
1617 NB2: the silent-superclass solution introduced new problems
1618 of its own, in the form of instance overlap. Tests
1619 SilentParametersOverlapping, T5051, and T7862 are examples
1620
1621 NB3: the silent-superclass solution also generated tons of
1622 extra dictionaries. For example, in monad-transformer
1623 code, when constructing a Monad dictionary you had to pass
1624 an Applicative dictionary; and to construct that you need
1625 a Functor dictionary. Yet these extra dictionaries were
1626 often never used. Test T3064 compiled *far* faster after
1627 silent superclasses were eliminated.
1628
1629 Our solution to this problem "silent superclass arguments". We pass
1630 to each dfun some ``silent superclass arguments’’, which are the
1631 immediate superclasses of the dictionary we are trying to
1632 construct. In our example:
1633 dfun :: forall a. C [a] -> D [a] -> D [a]
1634 dfun = \(dc::C [a]) (dd::D [a]) -> DOrd dc ...
1635 Notice the extra (dc :: C [a]) argument compared to the previous version.
1636
1637 This gives us:
1638
1639 -----------------------------------------------------------
1640 DFun Superclass Invariant
1641 ~~~~~~~~~~~~~~~~~~~~~~~~
1642 In the body of a DFun, every superclass argument to the
1643 returned dictionary is
1644 either * one of the arguments of the DFun,
1645 or * constant, bound at top level
1646 -----------------------------------------------------------
1647
1648 This net effect is that it is safe to treat a dfun application as
1649 wrapping a dictionary constructor around its arguments (in particular,
1650 a dfun never picks superclasses from the arguments under the
1651 dictionary constructor). No superclass is hidden inside a dfun
1652 application.
1653
1654 The extra arguments required to satisfy the DFun Superclass Invariant
1655 always come first, and are called the "silent" arguments. You can
1656 find out how many silent arguments there are using Id.dfunNSilent;
1657 and then you can just drop that number of arguments to see the ones
1658 that were in the original instance declaration.
1659
1660 DFun types are built (only) by MkId.mkDictFunId, so that is where we
1661 decide what silent arguments are to be added.
1662 -}
1663
1664 {-
1665 ************************************************************************
1666 * *
1667 Type-checking an instance method
1668 * *
1669 ************************************************************************
1670
1671 tcMethod
1672 - Make the method bindings, as a [(NonRec, HsBinds)], one per method
1673 - Remembering to use fresh Name (the instance method Name) as the binder
1674 - Bring the instance method Ids into scope, for the benefit of tcInstSig
1675 - Use sig_fn mapping instance method Name -> instance tyvars
1676 - Ditto prag_fn
1677 - Use tcValBinds to do the checking
1678 -}
1679
1680 tcMethods :: DFunId -> Class
1681 -> [TcTyVar] -> [EvVar]
1682 -> [TcType]
1683 -> TcEvBinds
1684 -> ([LTcSpecPrag], TcPragEnv)
1685 -> [ClassOpItem]
1686 -> InstBindings GhcRn
1687 -> TcM ([Id], LHsBinds GhcTc, Bag Implication)
1688 -- The returned inst_meth_ids all have types starting
1689 -- forall tvs. theta => ...
1690 tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
1691 dfun_ev_binds (spec_inst_prags, prag_fn) op_items
1692 (InstBindings { ib_binds = binds
1693 , ib_tyvars = lexical_tvs
1694 , ib_pragmas = sigs
1695 , ib_extensions = exts
1696 , ib_derived = is_derived })
1697 = tcExtendNameTyVarEnv (lexical_tvs `zip` tyvars) $
1698 -- The lexical_tvs scope over the 'where' part
1699 do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
1700 ; checkMinimalDefinition
1701 ; checkMethBindMembership
1702 ; (ids, binds, mb_implics) <- set_exts exts $
1703 unset_warnings_deriving $
1704 mapAndUnzip3M tc_item op_items
1705 ; return (ids, listToBag binds, listToBag (catMaybes mb_implics)) }
1706 where
1707 set_exts :: [LangExt.Extension] -> TcM a -> TcM a
1708 set_exts es thing = foldr setXOptM thing es
1709
1710 -- See Note [Avoid -Winaccessible-code when deriving]
1711 unset_warnings_deriving :: TcM a -> TcM a
1712 unset_warnings_deriving
1713 | is_derived = unsetWOptM Opt_WarnInaccessibleCode
1714 | otherwise = id
1715
1716 hs_sig_fn = mkHsSigFun sigs
1717 inst_loc = getSrcSpan dfun_id
1718
1719 ----------------------
1720 tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
1721 tc_item (sel_id, dm_info)
1722 | Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
1723 = tcMethodBody clas tyvars dfun_ev_vars inst_tys
1724 dfun_ev_binds is_derived hs_sig_fn
1725 spec_inst_prags prags
1726 sel_id user_bind bndr_loc
1727 | otherwise
1728 = do { traceTc "tc_def" (ppr sel_id)
1729 ; tc_default sel_id dm_info }
1730
1731 ----------------------
1732 tc_default :: Id -> DefMethInfo
1733 -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
1734
1735 tc_default sel_id (Just (dm_name, _))
1736 = do { (meth_bind, inline_prags) <- mkDefMethBind dfun_id clas sel_id dm_name
1737 ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
1738 dfun_ev_binds is_derived hs_sig_fn
1739 spec_inst_prags inline_prags
1740 sel_id meth_bind inst_loc }
1741
1742 tc_default sel_id Nothing -- No default method at all
1743 = do { traceTc "tc_def: warn" (ppr sel_id)
1744 ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
1745 inst_tys sel_id
1746 ; dflags <- getDynFlags
1747 ; let meth_bind = mkVarBind meth_id $
1748 mkLHsWrap lam_wrapper (error_rhs dflags)
1749 ; return (meth_id, meth_bind, Nothing) }
1750 where
1751 inst_loc' = noAnnSrcSpan inst_loc
1752 error_rhs dflags = L inst_loc'
1753 $ HsApp noComments error_fun (error_msg dflags)
1754 error_fun = L inst_loc' $
1755 wrapId (mkWpTyApps
1756 [ getRuntimeRep meth_tau, meth_tau])
1757 nO_METHOD_BINDING_ERROR_ID
1758 error_msg dflags = L inst_loc'
1759 (HsLit noComments (HsStringPrim NoSourceText
1760 (unsafeMkByteString (error_string dflags))))
1761 meth_tau = classMethodInstTy sel_id inst_tys
1762 error_string dflags = showSDoc dflags
1763 (hcat [ppr inst_loc, vbar, ppr sel_id ])
1764 lam_wrapper = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars
1765
1766 ----------------------
1767 -- Check if one of the minimal complete definitions is satisfied
1768 checkMinimalDefinition
1769 = whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $
1770 warnUnsatisfiedMinimalDefinition
1771
1772 methodExists meth = isJust (findMethodBind meth binds prag_fn)
1773
1774 ----------------------
1775 -- Check if any method bindings do not correspond to the class.
1776 -- See Note [Mismatched class methods and associated type families].
1777 checkMethBindMembership
1778 = mapM_ (addErrTc . badMethodErr clas) mismatched_meths
1779 where
1780 bind_nms = map unLoc $ collectMethodBinders binds
1781 cls_meth_nms = map (idName . fst) op_items
1782 mismatched_meths = bind_nms `minusList` cls_meth_nms
1783
1784 {-
1785 Note [Mismatched class methods and associated type families]
1786 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1787 It's entirely possible for someone to put methods or associated type family
1788 instances inside of a class in which it doesn't belong. For instance, we'd
1789 want to fail if someone wrote this:
1790
1791 instance Eq () where
1792 type Rep () = Maybe
1793 compare = undefined
1794
1795 Since neither the type family `Rep` nor the method `compare` belong to the
1796 class `Eq`. Normally, this is caught in the renamer when resolving RdrNames,
1797 since that would discover that the parent class `Eq` is incorrect.
1798
1799 However, there is a scenario in which the renamer could fail to catch this:
1800 if the instance was generated through Template Haskell, as in #12387. In that
1801 case, Template Haskell will provide fully resolved names (e.g.,
1802 `GHC.Classes.compare`), so the renamer won't notice the sleight-of-hand going
1803 on. For this reason, we also put an extra validity check for this in the
1804 typechecker as a last resort.
1805
1806 Note [Avoid -Winaccessible-code when deriving]
1807 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1808 -Winaccessible-code can be particularly noisy when deriving instances for
1809 GADTs. Consider the following example (adapted from #8128):
1810
1811 data T a where
1812 MkT1 :: Int -> T Int
1813 MkT2 :: T Bool
1814 MkT3 :: T Bool
1815 deriving instance Eq (T a)
1816 deriving instance Ord (T a)
1817
1818 In the derived Ord instance, GHC will generate the following code:
1819
1820 instance Ord (T a) where
1821 compare x y
1822 = case x of
1823 MkT2
1824 -> case y of
1825 MkT1 {} -> GT
1826 MkT2 -> EQ
1827 _ -> LT
1828 ...
1829
1830 However, that MkT1 is unreachable, since the type indices for MkT1 and MkT2
1831 differ, so if -Winaccessible-code is enabled, then deriving this instance will
1832 result in unwelcome warnings.
1833
1834 One conceivable approach to fixing this issue would be to change `deriving Ord`
1835 such that it becomes smarter about not generating unreachable cases. This,
1836 however, would be a highly nontrivial refactor, as we'd have to propagate
1837 through typing information everywhere in the algorithm that generates Ord
1838 instances in order to determine which cases were unreachable. This seems like
1839 a lot of work for minimal gain, so we have opted not to go for this approach.
1840
1841 Instead, we take the much simpler approach of always disabling
1842 -Winaccessible-code for derived code. To accomplish this, we do the following:
1843
1844 1. In tcMethods (which typechecks method bindings), disable
1845 -Winaccessible-code.
1846 2. When creating Implications during typechecking, record this flag
1847 (in ic_warn_inaccessible) at the time of creation.
1848 3. After typechecking comes error reporting, where GHC must decide how to
1849 report inaccessible code to the user, on an Implication-by-Implication
1850 basis. If an Implication's DynFlags indicate that -Winaccessible-code was
1851 disabled, then don't bother reporting it. That's it!
1852 -}
1853
1854 ------------------------
1855 tcMethodBody :: Class -> [TcTyVar] -> [EvVar] -> [TcType]
1856 -> TcEvBinds -> Bool
1857 -> HsSigFun
1858 -> [LTcSpecPrag] -> [LSig GhcRn]
1859 -> Id -> LHsBind GhcRn -> SrcSpan
1860 -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
1861 tcMethodBody clas tyvars dfun_ev_vars inst_tys
1862 dfun_ev_binds is_derived
1863 sig_fn spec_inst_prags prags
1864 sel_id (L bind_loc meth_bind) bndr_loc
1865 = add_meth_ctxt $
1866 do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc)
1867 ; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $
1868 mkMethIds clas tyvars dfun_ev_vars
1869 inst_tys sel_id
1870
1871 ; let lm_bind = meth_bind { fun_id = L (noAnnSrcSpan bndr_loc)
1872 (idName local_meth_id) }
1873 -- Substitute the local_meth_name for the binder
1874 -- NB: the binding is always a FunBind
1875
1876 -- taking instance signature into account might change the type of
1877 -- the local_meth_id
1878 ; (meth_implic, ev_binds_var, tc_bind)
1879 <- checkInstConstraints $
1880 tcMethodBodyHelp sig_fn sel_id local_meth_id (L bind_loc lm_bind)
1881
1882 ; global_meth_id <- addInlinePrags global_meth_id prags
1883 ; spec_prags <- tcSpecPrags global_meth_id prags
1884
1885 ; let specs = mk_meth_spec_prags global_meth_id spec_inst_prags spec_prags
1886 export = ABE { abe_ext = noExtField
1887 , abe_poly = global_meth_id
1888 , abe_mono = local_meth_id
1889 , abe_wrap = idHsWrapper
1890 , abe_prags = specs }
1891
1892 local_ev_binds = TcEvBinds ev_binds_var
1893 full_bind = AbsBinds { abs_ext = noExtField
1894 , abs_tvs = tyvars
1895 , abs_ev_vars = dfun_ev_vars
1896 , abs_exports = [export]
1897 , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
1898 , abs_binds = tc_bind
1899 , abs_sig = True }
1900
1901 ; return (global_meth_id, L bind_loc full_bind, Just meth_implic) }
1902 where
1903 -- For instance decls that come from deriving clauses
1904 -- we want to print out the full source code if there's an error
1905 -- because otherwise the user won't see the code at all
1906 add_meth_ctxt thing
1907 | is_derived = addLandmarkErrCtxt (derivBindCtxt sel_id clas inst_tys) thing
1908 | otherwise = thing
1909
1910 tcMethodBodyHelp :: HsSigFun -> Id -> TcId
1911 -> LHsBind GhcRn -> TcM (LHsBinds GhcTc)
1912 tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
1913 | Just hs_sig_ty <- hs_sig_fn sel_name
1914 -- There is a signature in the instance
1915 -- See Note [Instance method signatures]
1916 = do { (sig_ty, hs_wrap)
1917 <- setSrcSpan (getLocA hs_sig_ty) $
1918 do { inst_sigs <- xoptM LangExt.InstanceSigs
1919 ; checkTc inst_sigs (misplacedInstSig sel_name hs_sig_ty)
1920 ; let ctxt = FunSigCtxt sel_name NoRRC
1921 ; sig_ty <- tcHsSigType ctxt hs_sig_ty
1922 ; let local_meth_ty = idType local_meth_id
1923 -- False <=> do not report redundant constraints when
1924 -- checking instance-sig <= class-meth-sig
1925 -- The instance-sig is the focus here; the class-meth-sig
1926 -- is fixed (#18036)
1927 ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
1928 tcSubTypeSigma ctxt sig_ty local_meth_ty
1929 ; return (sig_ty, hs_wrap) }
1930
1931 ; inner_meth_name <- newName (nameOccName sel_name)
1932 ; let ctxt = FunSigCtxt sel_name (lhsSigTypeContextSpan hs_sig_ty)
1933 -- WantRCC <=> check for redundant constraints in the
1934 -- user-specified instance signature
1935 inner_meth_id = mkLocalId inner_meth_name Many sig_ty
1936 inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id
1937 , sig_ctxt = ctxt
1938 , sig_loc = getLocA hs_sig_ty }
1939
1940
1941 ; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
1942
1943 ; let export = ABE { abe_ext = noExtField
1944 , abe_poly = local_meth_id
1945 , abe_mono = inner_id
1946 , abe_wrap = hs_wrap
1947 , abe_prags = noSpecPrags }
1948
1949 ; return (unitBag $ L (getLoc meth_bind) $
1950 AbsBinds { abs_ext = noExtField, abs_tvs = [], abs_ev_vars = []
1951 , abs_exports = [export]
1952 , abs_binds = tc_bind, abs_ev_binds = []
1953 , abs_sig = True }) }
1954
1955 | otherwise -- No instance signature
1956 = do { let ctxt = FunSigCtxt sel_name NoRRC
1957 -- NoRRC <=> don't report redundant constraints
1958 -- The signature is not under the users control!
1959 tc_sig = completeSigFromId ctxt local_meth_id
1960 -- Absent a type sig, there are no new scoped type variables here
1961 -- Only the ones from the instance decl itself, which are already
1962 -- in scope. Example:
1963 -- class C a where { op :: forall b. Eq b => ... }
1964 -- instance C [c] where { op = <rhs> }
1965 -- In <rhs>, 'c' is scope but 'b' is not!
1966
1967 ; (tc_bind, _) <- tcPolyCheck no_prag_fn tc_sig meth_bind
1968 ; return tc_bind }
1969
1970 where
1971 sel_name = idName sel_id
1972 no_prag_fn = emptyPragEnv -- No pragmas for local_meth_id;
1973 -- they are all for meth_id
1974
1975 ------------------------
1976 mkMethIds :: Class -> [TcTyVar] -> [EvVar]
1977 -> [TcType] -> Id -> TcM (TcId, TcId)
1978 -- returns (poly_id, local_id), but ignoring any instance signature
1979 -- See Note [Instance method signatures]
1980 mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id
1981 = do { poly_meth_name <- newName (mkClassOpAuxOcc sel_occ)
1982 ; local_meth_name <- newName sel_occ
1983 -- Base the local_meth_name on the selector name, because
1984 -- type errors from tcMethodBody come from here
1985 ; let poly_meth_id = mkLocalId poly_meth_name Many poly_meth_ty
1986 local_meth_id = mkLocalId local_meth_name Many local_meth_ty
1987
1988 ; return (poly_meth_id, local_meth_id) }
1989 where
1990 sel_name = idName sel_id
1991 -- Force so that a thunk doesn't end up in a Name (#19619)
1992 !sel_occ = nameOccName sel_name
1993 local_meth_ty = instantiateMethod clas sel_id inst_tys
1994 poly_meth_ty = mkSpecSigmaTy tyvars theta local_meth_ty
1995 theta = map idType dfun_ev_vars
1996
1997 methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
1998 methSigCtxt sel_name sig_ty meth_ty env0
1999 = do { (env1, sig_ty) <- zonkTidyTcType env0 sig_ty
2000 ; (env2, meth_ty) <- zonkTidyTcType env1 meth_ty
2001 ; let msg = hang (text "When checking that instance signature for" <+> quotes (ppr sel_name))
2002 2 (vcat [ text "is more general than its signature in the class"
2003 , text "Instance sig:" <+> ppr sig_ty
2004 , text " Class sig:" <+> ppr meth_ty ])
2005 ; return (env2, msg) }
2006
2007 misplacedInstSig :: Name -> LHsSigType GhcRn -> TcRnMessage
2008 misplacedInstSig name hs_ty
2009 = TcRnUnknownMessage $ mkPlainError noHints $
2010 vcat [ hang (text "Illegal type signature in instance declaration:")
2011 2 (hang (pprPrefixName name)
2012 2 (dcolon <+> ppr hs_ty))
2013 , text "(Use InstanceSigs to allow this)" ]
2014
2015 {- Note [Instance method signatures]
2016 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2017 With -XInstanceSigs we allow the user to supply a signature for the
2018 method in an instance declaration. Here is an artificial example:
2019
2020 data T a = MkT a
2021 instance Ord a => Ord (T a) where
2022 (>) :: forall b. b -> b -> Bool
2023 (>) = error "You can't compare Ts"
2024
2025 The instance signature can be *more* polymorphic than the instantiated
2026 class method (in this case: Age -> Age -> Bool), but it cannot be less
2027 polymorphic. Moreover, if a signature is given, the implementation
2028 code should match the signature, and type variables bound in the
2029 singature should scope over the method body.
2030
2031 We achieve this by building a TcSigInfo for the method, whether or not
2032 there is an instance method signature, and using that to typecheck
2033 the declaration (in tcMethodBody). That means, conveniently,
2034 that the type variables bound in the signature will scope over the body.
2035
2036 What about the check that the instance method signature is more
2037 polymorphic than the instantiated class method type? We just do a
2038 tcSubType call in tcMethodBodyHelp, and generate a nested AbsBind, like
2039 this (for the example above
2040
2041 AbsBind { abs_tvs = [a], abs_ev_vars = [d:Ord a]
2042 , abs_exports
2043 = ABExport { (>) :: forall a. Ord a => T a -> T a -> Bool
2044 , gr_lcl :: T a -> T a -> Bool }
2045 , abs_binds
2046 = AbsBind { abs_tvs = [], abs_ev_vars = []
2047 , abs_exports = ABExport { gr_lcl :: T a -> T a -> Bool
2048 , gr_inner :: forall b. b -> b -> Bool }
2049 , abs_binds = AbsBind { abs_tvs = [b], abs_ev_vars = []
2050 , ..etc.. }
2051 } }
2052
2053 Wow! Three nested AbsBinds!
2054 * The outer one abstracts over the tyvars and dicts for the instance
2055 * The middle one is only present if there is an instance signature,
2056 and does the impedance matching for that signature
2057 * The inner one is for the method binding itself against either the
2058 signature from the class, or the instance signature.
2059 -}
2060
2061 ----------------------
2062 mk_meth_spec_prags :: Id -> [LTcSpecPrag] -> [LTcSpecPrag] -> TcSpecPrags
2063 -- Adapt the 'SPECIALISE instance' pragmas to work for this method Id
2064 -- There are two sources:
2065 -- * spec_prags_for_me: {-# SPECIALISE op :: <blah> #-}
2066 -- * spec_prags_from_inst: derived from {-# SPECIALISE instance :: <blah> #-}
2067 -- These ones have the dfun inside, but [perhaps surprisingly]
2068 -- the correct wrapper.
2069 -- See Note [Handling SPECIALISE pragmas] in GHC.Tc.Gen.Bind
2070 mk_meth_spec_prags meth_id spec_inst_prags spec_prags_for_me
2071 = SpecPrags (spec_prags_for_me ++ spec_prags_from_inst)
2072 where
2073 spec_prags_from_inst
2074 | isInlinePragma (idInlinePragma meth_id)
2075 = [] -- Do not inherit SPECIALISE from the instance if the
2076 -- method is marked INLINE, because then it'll be inlined
2077 -- and the specialisation would do nothing. (Indeed it'll provoke
2078 -- a warning from the desugarer
2079 | otherwise
2080 = [ L inst_loc (SpecPrag meth_id wrap inl)
2081 | L inst_loc (SpecPrag _ wrap inl) <- spec_inst_prags]
2082
2083
2084 mkDefMethBind :: DFunId -> Class -> Id -> Name
2085 -> TcM (LHsBind GhcRn, [LSig GhcRn])
2086 -- The is a default method (vanailla or generic) defined in the class
2087 -- So make a binding op = $dmop @t1 @t2
2088 -- where $dmop is the name of the default method in the class,
2089 -- and t1,t2 are the instance types.
2090 -- See Note [Default methods in instances] for why we use
2091 -- visible type application here
2092 mkDefMethBind dfun_id clas sel_id dm_name
2093 = do { logger <- getLogger
2094 ; dm_id <- tcLookupId dm_name
2095 ; let inline_prag = idInlinePragma dm_id
2096 inline_prags | isAnyInlinePragma inline_prag
2097 = [noLocA (InlineSig noAnn fn inline_prag)]
2098 | otherwise
2099 = []
2100 -- Copy the inline pragma (if any) from the default method
2101 -- to this version. Note [INLINE and default methods]
2102
2103 fn = noLocA (idName sel_id)
2104 visible_inst_tys = [ ty | (tcb, ty) <- tyConBinders (classTyCon clas) `zip` inst_tys
2105 , tyConBinderArgFlag tcb /= Inferred ]
2106 rhs = foldl' mk_vta (nlHsVar dm_name) visible_inst_tys
2107 bind = noLocA $ mkTopFunBind Generated fn $
2108 [mkSimpleMatch (mkPrefixFunRhs fn) [] rhs]
2109
2110 ; liftIO (putDumpFileMaybe logger Opt_D_dump_deriv "Filling in method body"
2111 FormatHaskell
2112 (vcat [ppr clas <+> ppr inst_tys,
2113 nest 2 (ppr sel_id <+> equals <+> ppr rhs)]))
2114
2115 ; return (bind, inline_prags) }
2116 where
2117 (_, _, _, inst_tys) = tcSplitDFunTy (idType dfun_id)
2118
2119 mk_vta :: LHsExpr GhcRn -> Type -> LHsExpr GhcRn
2120 mk_vta fun ty = noLocA (HsAppType noExtField fun (mkEmptyWildCardBndrs $ nlHsParTy
2121 $ noLocA $ XHsType ty))
2122 -- NB: use visible type application
2123 -- See Note [Default methods in instances]
2124
2125 ----------------------
2126 derivBindCtxt :: Id -> Class -> [Type ] -> SDoc
2127 derivBindCtxt sel_id clas tys
2128 = vcat [ text "When typechecking the code for" <+> quotes (ppr sel_id)
2129 , nest 2 (text "in a derived instance for"
2130 <+> quotes (pprClassPred clas tys) <> colon)
2131 , nest 2 $ text "To see the code I am typechecking, use -ddump-deriv" ]
2132
2133 warnUnsatisfiedMinimalDefinition :: ClassMinimalDef -> TcM ()
2134 warnUnsatisfiedMinimalDefinition mindef
2135 = do { warn <- woptM Opt_WarnMissingMethods
2136 ; let msg = TcRnUnknownMessage $
2137 mkPlainDiagnostic (WarningWithFlag Opt_WarnMissingMethods) noHints message
2138 ; diagnosticTc warn msg
2139 }
2140 where
2141 message = vcat [text "No explicit implementation for"
2142 ,nest 2 $ pprBooleanFormulaNice mindef
2143 ]
2144
2145 {-
2146 Note [Export helper functions]
2147 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2148 We arrange to export the "helper functions" of an instance declaration,
2149 so that they are not subject to preInlineUnconditionally, even if their
2150 RHS is trivial. Reason: they are mentioned in the DFunUnfolding of
2151 the dict fun as Ids, not as CoreExprs, so we can't substitute a
2152 non-variable for them.
2153
2154 We could change this by making DFunUnfoldings have CoreExprs, but it
2155 seems a bit simpler this way.
2156
2157 Note [Default methods in instances]
2158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2159 Consider this
2160
2161 class Baz v x where
2162 foo :: x -> x
2163 foo y = <blah>
2164
2165 instance Baz Int Int
2166
2167 From the class decl we get
2168
2169 $dmfoo :: forall v x. Baz v x => x -> x
2170 $dmfoo y = <blah>
2171
2172 Notice that the type is ambiguous. So we use Visible Type Application
2173 to disambiguate:
2174
2175 $dBazIntInt = MkBaz fooIntInt
2176 fooIntInt = $dmfoo @Int @Int
2177
2178 Lacking VTA we'd get ambiguity errors involving the default method. This applies
2179 equally to vanilla default methods (#1061) and generic default methods
2180 (#12220).
2181
2182 Historical note: before we had VTA we had to generate
2183 post-type-checked code, which took a lot more code, and didn't work for
2184 generic default methods.
2185
2186 Note [INLINE and default methods]
2187 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2188 Default methods need special case. They are supposed to behave rather like
2189 macros. For example
2190
2191 class Foo a where
2192 op1, op2 :: Bool -> a -> a
2193
2194 {-# INLINE op1 #-}
2195 op1 b x = op2 (not b) x
2196
2197 instance Foo Int where
2198 -- op1 via default method
2199 op2 b x = <blah>
2200
2201 The instance declaration should behave
2202
2203 just as if 'op1' had been defined with the
2204 code, and INLINE pragma, from its original
2205 definition.
2206
2207 That is, just as if you'd written
2208
2209 instance Foo Int where
2210 op2 b x = <blah>
2211
2212 {-# INLINE op1 #-}
2213 op1 b x = op2 (not b) x
2214
2215 So for the above example we generate:
2216
2217 {-# INLINE $dmop1 #-}
2218 -- $dmop1 has an InlineCompulsory unfolding
2219 $dmop1 d b x = op2 d (not b) x
2220
2221 $fFooInt = MkD $cop1 $cop2
2222
2223 {-# INLINE $cop1 #-}
2224 $cop1 = $dmop1 $fFooInt
2225
2226 $cop2 = <blah>
2227
2228 Note carefully:
2229
2230 * We *copy* any INLINE pragma from the default method $dmop1 to the
2231 instance $cop1. Otherwise we'll just inline the former in the
2232 latter and stop, which isn't what the user expected
2233
2234 * Regardless of its pragma, we give the default method an
2235 unfolding with an InlineCompulsory source. That means
2236 that it'll be inlined at every use site, notably in
2237 each instance declaration, such as $cop1. This inlining
2238 must happen even though
2239 a) $dmop1 is not saturated in $cop1
2240 b) $cop1 itself has an INLINE pragma
2241
2242 It's vital that $dmop1 *is* inlined in this way, to allow the mutual
2243 recursion between $fooInt and $cop1 to be broken
2244
2245 * To communicate the need for an InlineCompulsory to the desugarer
2246 (which makes the Unfoldings), we use the IsDefaultMethod constructor
2247 in TcSpecPrags.
2248
2249
2250 ************************************************************************
2251 * *
2252 Specialise instance pragmas
2253 * *
2254 ************************************************************************
2255
2256 Note [SPECIALISE instance pragmas]
2257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2258 Consider
2259
2260 instance (Ix a, Ix b) => Ix (a,b) where
2261 {-# SPECIALISE instance Ix (Int,Int) #-}
2262 range (x,y) = ...
2263
2264 We make a specialised version of the dictionary function, AND
2265 specialised versions of each *method*. Thus we should generate
2266 something like this:
2267
2268 $dfIxPair :: (Ix a, Ix b) => Ix (a,b)
2269 {-# DFUN [$crangePair, ...] #-}
2270 {-# SPECIALISE $dfIxPair :: Ix (Int,Int) #-}
2271 $dfIxPair da db = Ix ($crangePair da db) (...other methods...)
2272
2273 $crange :: (Ix a, Ix b) -> ((a,b),(a,b)) -> [(a,b)]
2274 {-# SPECIALISE $crange :: ((Int,Int),(Int,Int)) -> [(Int,Int)] #-}
2275 $crange da db = <blah>
2276
2277 The SPECIALISE pragmas are acted upon by the desugarer, which generate
2278
2279 dii :: Ix Int
2280 dii = ...
2281
2282 $s$dfIxPair :: Ix ((Int,Int),(Int,Int))
2283 {-# DFUN [$crangePair di di, ...] #-}
2284 $s$dfIxPair = Ix ($crangePair di di) (...)
2285
2286 {-# RULE forall (d1,d2:Ix Int). $dfIxPair Int Int d1 d2 = $s$dfIxPair #-}
2287
2288 $s$crangePair :: ((Int,Int),(Int,Int)) -> [(Int,Int)]
2289 $c$crangePair = ...specialised RHS of $crangePair...
2290
2291 {-# RULE forall (d1,d2:Ix Int). $crangePair Int Int d1 d2 = $s$crangePair #-}
2292
2293 Note that
2294
2295 * The specialised dictionary $s$dfIxPair is very much needed, in case we
2296 call a function that takes a dictionary, but in a context where the
2297 specialised dictionary can be used. See #7797.
2298
2299 * The ClassOp rule for 'range' works equally well on $s$dfIxPair, because
2300 it still has a DFunUnfolding. See Note [ClassOp/DFun selection]
2301
2302 * A call (range ($dfIxPair Int Int d1 d2)) might simplify two ways:
2303 --> {ClassOp rule for range} $crangePair Int Int d1 d2
2304 --> {SPEC rule for $crangePair} $s$crangePair
2305 or thus:
2306 --> {SPEC rule for $dfIxPair} range $s$dfIxPair
2307 --> {ClassOpRule for range} $s$crangePair
2308 It doesn't matter which way.
2309
2310 * We want to specialise the RHS of both $dfIxPair and $crangePair,
2311 but the SAME HsWrapper will do for both! We can call tcSpecPrag
2312 just once, and pass the result (in spec_inst_info) to tcMethods.
2313 -}
2314
2315 tcSpecInstPrags :: DFunId -> InstBindings GhcRn
2316 -> TcM ([LTcSpecPrag], TcPragEnv)
2317 tcSpecInstPrags dfun_id (InstBindings { ib_binds = binds, ib_pragmas = uprags })
2318 = do { spec_inst_prags <- mapM (wrapLocAM (tcSpecInst dfun_id)) $
2319 filter isSpecInstLSig uprags
2320 -- The filter removes the pragmas for methods
2321 ; return (spec_inst_prags, mkPragEnv uprags binds) }
2322
2323 ------------------------------
2324 tcSpecInst :: Id -> Sig GhcRn -> TcM TcSpecPrag
2325 tcSpecInst dfun_id prag@(SpecInstSig _ _ hs_ty)
2326 = addErrCtxt (spec_ctxt prag) $
2327 do { spec_dfun_ty <- tcHsClsInstType SpecInstCtxt hs_ty
2328 ; co_fn <- tcSpecWrapper SpecInstCtxt (idType dfun_id) spec_dfun_ty
2329 ; return (SpecPrag dfun_id co_fn defaultInlinePragma) }
2330 where
2331 spec_ctxt prag = hang (text "In the pragma:") 2 (ppr prag)
2332
2333 tcSpecInst _ _ = panic "tcSpecInst"
2334
2335 {-
2336 ************************************************************************
2337 * *
2338 \subsection{Error messages}
2339 * *
2340 ************************************************************************
2341 -}
2342
2343 instDeclCtxt1 :: LHsSigType GhcRn -> SDoc
2344 instDeclCtxt1 hs_inst_ty
2345 = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
2346
2347 instDeclCtxt2 :: Type -> SDoc
2348 instDeclCtxt2 dfun_ty
2349 = inst_decl_ctxt (ppr (mkClassPred cls tys))
2350 where
2351 (_,_,cls,tys) = tcSplitDFunTy dfun_ty
2352
2353 inst_decl_ctxt :: SDoc -> SDoc
2354 inst_decl_ctxt doc = hang (text "In the instance declaration for")
2355 2 (quotes doc)
2356
2357 badBootFamInstDeclErr :: TcRnMessage
2358 badBootFamInstDeclErr
2359 = TcRnUnknownMessage $ mkPlainError noHints $ text "Illegal family instance in hs-boot file"
2360
2361 notFamily :: TyCon -> TcRnMessage
2362 notFamily tycon
2363 = TcRnUnknownMessage $ mkPlainError noHints $
2364 vcat [ text "Illegal family instance for" <+> quotes (ppr tycon)
2365 , nest 2 $ parens (ppr tycon <+> text "is not an indexed type family")]
2366
2367 assocInClassErr :: TyCon -> TcRnMessage
2368 assocInClassErr name
2369 = TcRnUnknownMessage $ mkPlainError noHints $
2370 text "Associated type" <+> quotes (ppr name) <+>
2371 text "must be inside a class instance"
2372
2373 badFamInstDecl :: TyCon -> TcRnMessage
2374 badFamInstDecl tc_name
2375 = TcRnUnknownMessage $ mkPlainError noHints $
2376 vcat [ text "Illegal family instance for" <+>
2377 quotes (ppr tc_name)
2378 , nest 2 (parens $ text "Use TypeFamilies to allow indexed type families") ]
2379
2380 notOpenFamily :: TyCon -> TcRnMessage
2381 notOpenFamily tc
2382 = TcRnUnknownMessage $ mkPlainError noHints $
2383 text "Illegal instance for closed family" <+> quotes (ppr tc)