Fix #13819 by refactoring TypeEqOrigin.uo_thing
[ghc.git] / compiler / typecheck / TcSigs.hs
1 {-
2 (c) The University of Glasgow 2006-2012
3 (c) The GRASP Project, Glasgow University, 1992-2002
4
5 -}
6
7 {-# LANGUAGE CPP #-}
8 {-# LANGUAGE TypeFamilies #-}
9
10 module TcSigs(
11 TcSigInfo(..),
12 TcIdSigInfo(..), TcIdSigInst,
13 TcPatSynInfo(..),
14 TcSigFun,
15
16 isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
17 completeSigPolyId_maybe,
18
19 tcTySigs, tcUserTypeSig, completeSigFromId,
20 tcInstSig,
21
22 TcPragEnv, emptyPragEnv, lookupPragEnv, extendPragEnv,
23 mkPragEnv, tcSpecPrags, tcSpecWrapper, tcImpPrags, addInlinePrags
24 ) where
25
26 #include "HsVersions.h"
27
28 import HsSyn
29 import TcHsType
30 import TcRnTypes
31 import TcRnMonad
32 import TcType
33 import TcMType
34 import TcValidity ( checkValidType )
35 import TcUnify( tcSkolemise, unifyType )
36 import Inst( topInstantiate )
37 import TcEnv( tcLookupId )
38 import TcEvidence( HsWrapper, (<.>) )
39 import Type( mkTyVarBinders )
40
41 import DynFlags
42 import Var ( TyVar, tyVarName, tyVarKind )
43 import Id ( Id, idName, idType, idInlinePragma, setInlinePragma, mkLocalId )
44 import PrelNames( mkUnboundName )
45 import BasicTypes
46 import Bag( foldrBag )
47 import Module( getModule )
48 import Name
49 import NameEnv
50 import VarSet
51 import Outputable
52 import SrcLoc
53 import Util( singleton )
54 import Maybes( orElse )
55 import Data.Maybe( mapMaybe )
56 import Control.Monad( unless )
57
58
59 {- -------------------------------------------------------------
60 Note [Overview of type signatures]
61 ----------------------------------------------------------------
62 Type signatures, including partial signatures, are jolly tricky,
63 especially on value bindings. Here's an overview.
64
65 f :: forall a. [a] -> [a]
66 g :: forall b. _ -> b
67
68 f = ...g...
69 g = ...f...
70
71 * HsSyn: a signature in a binding starts of as a TypeSig, in
72 type HsBinds.Sig
73
74 * When starting a mutually recursive group, like f/g above, we
75 call tcTySig on each signature in the group.
76
77 * tcTySig: Sig -> TcIdSigInfo
78 - For a /complete/ signature, like 'f' above, tcTySig kind-checks
79 the HsType, producing a Type, and wraps it in a CompleteSig, and
80 extend the type environment with this polymorphic 'f'.
81
82 - For a /partial/signature, like 'g' above, tcTySig does nothing
83 Instead it just wraps the pieces in a PartialSig, to be handled
84 later.
85
86 * tcInstSig: TcIdSigInfo -> TcIdSigInst
87 In tcMonoBinds, when looking at an individual binding, we use
88 tcInstSig to instantiate the signature forall's in the signature,
89 and attribute that instantiated (monomorphic) type to the
90 binder. You can see this in TcBinds.tcLhsId.
91
92 The instantiation does the obvious thing for complete signatures,
93 but for /partial/ signatures it starts from the HsSyn, so it
94 has to kind-check it etc: tcHsPartialSigType. It's convenient
95 to do this at the same time as instantiation, because we can
96 make the wildcards into unification variables right away, raather
97 than somehow quantifying over them. And the "TcLevel" of those
98 unification variables is correct because we are in tcMonoBinds.
99
100
101 Note [Scoped tyvars]
102 ~~~~~~~~~~~~~~~~~~~~
103 The -XScopedTypeVariables flag brings lexically-scoped type variables
104 into scope for any explicitly forall-quantified type variables:
105 f :: forall a. a -> a
106 f x = e
107 Then 'a' is in scope inside 'e'.
108
109 However, we do *not* support this
110 - For pattern bindings e.g
111 f :: forall a. a->a
112 (f,g) = e
113
114 Note [Binding scoped type variables]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 The type variables *brought into lexical scope* by a type signature
117 may be a subset of the *quantified type variables* of the signatures,
118 for two reasons:
119
120 * With kind polymorphism a signature like
121 f :: forall f a. f a -> f a
122 may actually give rise to
123 f :: forall k. forall (f::k -> *) (a:k). f a -> f a
124 So the sig_tvs will be [k,f,a], but only f,a are scoped.
125 NB: the scoped ones are not necessarily the *inital* ones!
126
127 * Even aside from kind polymorphism, there may be more instantiated
128 type variables than lexically-scoped ones. For example:
129 type T a = forall b. b -> (a,b)
130 f :: forall c. T c
131 Here, the signature for f will have one scoped type variable, c,
132 but two instantiated type variables, c' and b'.
133
134 However, all of this only applies to the renamer. The typechecker
135 just puts all of them into the type environment; any lexical-scope
136 errors were dealt with by the renamer.
137
138 -}
139
140
141 {- *********************************************************************
142 * *
143 Utility functions for TcSigInfo
144 * *
145 ********************************************************************* -}
146
147 tcIdSigName :: TcIdSigInfo -> Name
148 tcIdSigName (CompleteSig { sig_bndr = id }) = idName id
149 tcIdSigName (PartialSig { psig_name = n }) = n
150
151 tcSigInfoName :: TcSigInfo -> Name
152 tcSigInfoName (TcIdSig idsi) = tcIdSigName idsi
153 tcSigInfoName (TcPatSynSig tpsi) = patsig_name tpsi
154
155 completeSigPolyId_maybe :: TcSigInfo -> Maybe TcId
156 completeSigPolyId_maybe sig
157 | TcIdSig sig_info <- sig
158 , CompleteSig { sig_bndr = id } <- sig_info = Just id
159 | otherwise = Nothing
160
161
162 {- *********************************************************************
163 * *
164 Typechecking user signatures
165 * *
166 ********************************************************************* -}
167
168 tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
169 tcTySigs hs_sigs
170 = checkNoErrs $ -- See Note [Fail eagerly on bad signatures]
171 do { ty_sigs_s <- mapAndRecoverM tcTySig hs_sigs
172 ; let ty_sigs = concat ty_sigs_s
173 poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs
174 -- The returned [TcId] are the ones for which we have
175 -- a complete type signature.
176 -- See Note [Complete and partial type signatures]
177 env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]
178 ; return (poly_ids, lookupNameEnv env) }
179
180 tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
181 tcTySig (L _ (IdSig id))
182 = do { let ctxt = FunSigCtxt (idName id) False
183 -- False: do not report redundant constraints
184 -- The user has no control over the signature!
185 sig = completeSigFromId ctxt id
186 ; return [TcIdSig sig] }
187
188 tcTySig (L loc (TypeSig names sig_ty))
189 = setSrcSpan loc $
190 do { sigs <- sequence [ tcUserTypeSig loc sig_ty (Just name)
191 | L _ name <- names ]
192 ; return (map TcIdSig sigs) }
193
194 tcTySig (L loc (PatSynSig names sig_ty))
195 = setSrcSpan loc $
196 do { tpsigs <- sequence [ tcPatSynSig name sig_ty
197 | L _ name <- names ]
198 ; return (map TcPatSynSig tpsigs) }
199
200 tcTySig _ = return []
201
202
203 tcUserTypeSig :: SrcSpan -> LHsSigWcType GhcRn -> Maybe Name
204 -> TcM TcIdSigInfo
205 -- A function or expression type signature
206 -- Returns a fully quantified type signature; even the wildcards
207 -- are quantified with ordinary skolems that should be instantiated
208 --
209 -- The SrcSpan is what to declare as the binding site of the
210 -- any skolems in the signature. For function signatures we
211 -- use the whole `f :: ty' signature; for expression signatures
212 -- just the type part.
213 --
214 -- Just n => Function type signature name :: type
215 -- Nothing => Expression type signature <expr> :: type
216 tcUserTypeSig loc hs_sig_ty mb_name
217 | isCompleteHsSig hs_sig_ty
218 = do { sigma_ty <- tcHsSigWcType ctxt_F hs_sig_ty
219 ; return $
220 CompleteSig { sig_bndr = mkLocalId name sigma_ty
221 , sig_ctxt = ctxt_T
222 , sig_loc = loc } }
223 -- Location of the <type> in f :: <type>
224
225 -- Partial sig with wildcards
226 | otherwise
227 = return (PartialSig { psig_name = name, psig_hs_ty = hs_sig_ty
228 , sig_ctxt = ctxt_F, sig_loc = loc })
229 where
230 name = case mb_name of
231 Just n -> n
232 Nothing -> mkUnboundName (mkVarOcc "<expression>")
233 ctxt_F = case mb_name of
234 Just n -> FunSigCtxt n False
235 Nothing -> ExprSigCtxt
236 ctxt_T = case mb_name of
237 Just n -> FunSigCtxt n True
238 Nothing -> ExprSigCtxt
239
240
241
242 completeSigFromId :: UserTypeCtxt -> Id -> TcIdSigInfo
243 -- Used for instance methods and record selectors
244 completeSigFromId ctxt id
245 = CompleteSig { sig_bndr = id
246 , sig_ctxt = ctxt
247 , sig_loc = getSrcSpan id }
248
249 isCompleteHsSig :: LHsSigWcType GhcRn -> Bool
250 -- ^ If there are no wildcards, return a LHsSigType
251 isCompleteHsSig (HsWC { hswc_wcs = wcs }) = null wcs
252
253 {- Note [Fail eagerly on bad signatures]
254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
255 If a type signature is wrong, fail immediately:
256
257 * the type sigs may bind type variables, so proceeding without them
258 can lead to a cascade of errors
259
260 * the type signature might be ambiguous, in which case checking
261 the code against the signature will give a very similar error
262 to the ambiguity error.
263
264 ToDo: this means we fall over if any type sig
265 is wrong (eg at the top level of the module),
266 which is over-conservative
267 -}
268
269 {- *********************************************************************
270 * *
271 Type checking a pattern synonym signature
272 * *
273 ************************************************************************
274
275 Note [Pattern synonym signatures]
276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
277 Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example).
278 In general they look like this:
279
280 pattern P :: forall univ_tvs. req_theta
281 => forall ex_tvs. prov_theta
282 => arg1 -> .. -> argn -> res_ty
283
284 For parsing and renaming we treat the signature as an ordinary LHsSigType.
285
286 Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
287
288 * Note that 'forall univ_tvs' and 'req_theta =>'
289 and 'forall ex_tvs' and 'prov_theta =>'
290 are all optional. We gather the pieces at the the top of tcPatSynSig
291
292 * Initially the implicitly-bound tyvars (added by the renamer) include both
293 universal and existential vars.
294
295 * After we kind-check the pieces and convert to Types, we do kind generalisation.
296
297 Note [The pattern-synonym signature splitting rule]
298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
299 Given a pattern signature, we must split
300 the kind-generalised variables, and
301 the implicitly-bound variables
302 into universal and existential. The rule is this
303 (see discussion on Trac #11224):
304
305 The universal tyvars are the ones mentioned in
306 - univ_tvs: the user-specified (forall'd) universals
307 - req_theta
308 - res_ty
309 The existential tyvars are all the rest
310
311 For example
312
313 pattern P :: () => b -> T a
314 pattern P x = ...
315
316 Here 'a' is universal, and 'b' is existential. But there is a wrinkle:
317 how do we split the arg_tys from req_ty? Consider
318
319 pattern Q :: () => b -> S c -> T a
320 pattern Q x = ...
321
322 This is an odd example because Q has only one syntactic argument, and
323 so presumably is defined by a view pattern matching a function. But
324 it can happen (Trac #11977, #12108).
325
326 We don't know Q's arity from the pattern signature, so we have to wait
327 until we see the pattern declaration itself before deciding res_ty is,
328 and hence which variables are existential and which are universal.
329
330 And that in turn is why TcPatSynInfo has a separate field,
331 patsig_implicit_bndrs, to capture the implicitly bound type variables,
332 because we don't yet know how to split them up.
333
334 It's a slight compromise, because it means we don't really know the
335 pattern synonym's real signature until we see its declaration. So,
336 for example, in hs-boot file, we may need to think what to do...
337 (eg don't have any implicitly-bound variables).
338 -}
339
340 tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
341 tcPatSynSig name sig_ty
342 | HsIB { hsib_vars = implicit_hs_tvs
343 , hsib_body = hs_ty } <- sig_ty
344 , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty
345 , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
346 = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, body_ty))
347 <- solveEqualities $
348 tcImplicitTKBndrs implicit_hs_tvs $
349 tcExplicitTKBndrs univ_hs_tvs $ \ univ_tvs ->
350 tcExplicitTKBndrs ex_hs_tvs $ \ ex_tvs ->
351 do { req <- tcHsContext hs_req
352 ; prov <- tcHsContext hs_prov
353 ; body_ty <- tcHsOpenType hs_body_ty
354 -- A (literal) pattern can be unlifted;
355 -- e.g. pattern Zero <- 0# (Trac #12094)
356 ; let bound_tvs
357 = unionVarSets [ allBoundVariabless req
358 , allBoundVariabless prov
359 , allBoundVariables body_ty
360 ]
361 ; return ( (univ_tvs, req, ex_tvs, prov, body_ty)
362 , bound_tvs) }
363
364 -- Kind generalisation
365 ; kvs <- kindGeneralize $
366 build_patsyn_type [] implicit_tvs univ_tvs req
367 ex_tvs prov body_ty
368
369 -- These are /signatures/ so we zonk to squeeze out any kind
370 -- unification variables. Do this after quantifyTyVars which may
371 -- default kind variables to *.
372 ; traceTc "about zonk" empty
373 ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
374 ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs
375 ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs
376 ; req <- zonkTcTypes req
377 ; prov <- zonkTcTypes prov
378 ; body_ty <- zonkTcType body_ty
379
380 -- Now do validity checking
381 ; checkValidType ctxt $
382 build_patsyn_type kvs implicit_tvs univ_tvs req ex_tvs prov body_ty
383
384 -- arguments become the types of binders. We thus cannot allow
385 -- levity polymorphism here
386 ; let (arg_tys, _) = tcSplitFunTys body_ty
387 ; mapM_ (checkForLevPoly empty) arg_tys
388
389 ; traceTc "tcTySig }" $
390 vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
391 , text "kvs" <+> ppr_tvs kvs
392 , text "univ_tvs" <+> ppr_tvs univ_tvs
393 , text "req" <+> ppr req
394 , text "ex_tvs" <+> ppr_tvs ex_tvs
395 , text "prov" <+> ppr prov
396 , text "body_ty" <+> ppr body_ty ]
397 ; return (TPSI { patsig_name = name
398 , patsig_implicit_bndrs = mkTyVarBinders Inferred kvs ++
399 mkTyVarBinders Specified implicit_tvs
400 , patsig_univ_bndrs = univ_tvs
401 , patsig_req = req
402 , patsig_ex_bndrs = ex_tvs
403 , patsig_prov = prov
404 , patsig_body_ty = body_ty }) }
405 where
406 ctxt = PatSynCtxt name
407
408 build_patsyn_type kvs imp univ req ex prov body
409 = mkInvForAllTys kvs $
410 mkSpecForAllTys (imp ++ univ) $
411 mkFunTys req $
412 mkSpecForAllTys ex $
413 mkFunTys prov $
414 body
415
416 ppr_tvs :: [TyVar] -> SDoc
417 ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
418 | tv <- tvs])
419
420
421 {- *********************************************************************
422 * *
423 Instantiating user signatures
424 * *
425 ********************************************************************* -}
426
427
428 tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
429 -- Instantiate a type signature; only used with plan InferGen
430 tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
431 = setSrcSpan loc $ -- Set the binding site of the tyvars
432 do { (tv_prs, theta, tau) <- tcInstType newMetaSigTyVars poly_id
433 -- See Note [Pattern bindings and complete signatures]
434
435 ; return (TISI { sig_inst_sig = sig
436 , sig_inst_skols = tv_prs
437 , sig_inst_wcs = []
438 , sig_inst_wcx = Nothing
439 , sig_inst_theta = theta
440 , sig_inst_tau = tau }) }
441
442 tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
443 , sig_ctxt = ctxt
444 , sig_loc = loc })
445 = setSrcSpan loc $ -- Set the binding site of the tyvars
446 do { (wcs, wcx, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
447 ; return (TISI { sig_inst_sig = sig
448 , sig_inst_skols = map (\tv -> (tyVarName tv, tv)) tvs
449 , sig_inst_wcs = wcs
450 , sig_inst_wcx = wcx
451 , sig_inst_theta = theta
452 , sig_inst_tau = tau }) }
453
454
455 {- Note [Pattern bindings and complete signatures]
456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
457 Consider
458 data T a = MkT a a
459 f :: forall a. a->a
460 g :: forall b. b->b
461 MkT f g = MkT (\x->x) (\y->y)
462 Here we'll infer a type from the pattern of 'T a', but if we feed in
463 the signature types for f and g, we'll end up unifying 'a' and 'b'
464
465 So we instantiate f and g's signature with SigTv skolems
466 (newMetaSigTyVars) that can unify with each other. If too much
467 unification takes place, we'll find out when we do the final
468 impedance-matching check in TcBinds.mkExport
469
470 See Note [Signature skolems] in TcType
471
472 None of this applies to a function binding with a complete
473 signature, which doesn't use tcInstSig. See TcBinds.tcPolyCheck.
474 -}
475
476 {- *********************************************************************
477 * *
478 Pragmas and PragEnv
479 * *
480 ********************************************************************* -}
481
482 type TcPragEnv = NameEnv [LSig GhcRn]
483
484 emptyPragEnv :: TcPragEnv
485 emptyPragEnv = emptyNameEnv
486
487 lookupPragEnv :: TcPragEnv -> Name -> [LSig GhcRn]
488 lookupPragEnv prag_fn n = lookupNameEnv prag_fn n `orElse` []
489
490 extendPragEnv :: TcPragEnv -> (Name, LSig GhcRn) -> TcPragEnv
491 extendPragEnv prag_fn (n, sig) = extendNameEnv_Acc (:) singleton prag_fn n sig
492
493 ---------------
494 mkPragEnv :: [LSig GhcRn] -> LHsBinds GhcRn -> TcPragEnv
495 mkPragEnv sigs binds
496 = foldl extendPragEnv emptyNameEnv prs
497 where
498 prs = mapMaybe get_sig sigs
499
500 get_sig :: LSig GhcRn -> Maybe (Name, LSig GhcRn)
501 get_sig (L l (SpecSig lnm@(L _ nm) ty inl)) = Just (nm, L l $ SpecSig lnm ty (add_arity nm inl))
502 get_sig (L l (InlineSig lnm@(L _ nm) inl)) = Just (nm, L l $ InlineSig lnm (add_arity nm inl))
503 get_sig (L l (SCCFunSig st lnm@(L _ nm) str)) = Just (nm, L l $ SCCFunSig st lnm str)
504 get_sig _ = Nothing
505
506 add_arity n inl_prag -- Adjust inl_sat field to match visible arity of function
507 | Inline <- inl_inline inl_prag
508 -- add arity only for real INLINE pragmas, not INLINABLE
509 = case lookupNameEnv ar_env n of
510 Just ar -> inl_prag { inl_sat = Just ar }
511 Nothing -> WARN( True, text "mkPragEnv no arity" <+> ppr n )
512 -- There really should be a binding for every INLINE pragma
513 inl_prag
514 | otherwise
515 = inl_prag
516
517 -- ar_env maps a local to the arity of its definition
518 ar_env :: NameEnv Arity
519 ar_env = foldrBag lhsBindArity emptyNameEnv binds
520
521 lhsBindArity :: LHsBind GhcRn -> NameEnv Arity -> NameEnv Arity
522 lhsBindArity (L _ (FunBind { fun_id = id, fun_matches = ms })) env
523 = extendNameEnv env (unLoc id) (matchGroupArity ms)
524 lhsBindArity _ env = env -- PatBind/VarBind
525
526
527 -----------------
528 addInlinePrags :: TcId -> [LSig GhcRn] -> TcM TcId
529 addInlinePrags poly_id prags_for_me
530 | inl@(L _ prag) : inls <- inl_prags
531 = do { traceTc "addInlinePrag" (ppr poly_id $$ ppr prag)
532 ; unless (null inls) (warn_multiple_inlines inl inls)
533 ; return (poly_id `setInlinePragma` prag) }
534 | otherwise
535 = return poly_id
536 where
537 inl_prags = [L loc prag | L loc (InlineSig _ prag) <- prags_for_me]
538
539 warn_multiple_inlines _ [] = return ()
540
541 warn_multiple_inlines inl1@(L loc prag1) (inl2@(L _ prag2) : inls)
542 | inlinePragmaActivation prag1 == inlinePragmaActivation prag2
543 , isEmptyInlineSpec (inlinePragmaSpec prag1)
544 = -- Tiresome: inl1 is put there by virtue of being in a hs-boot loop
545 -- and inl2 is a user NOINLINE pragma; we don't want to complain
546 warn_multiple_inlines inl2 inls
547 | otherwise
548 = setSrcSpan loc $
549 addWarnTc NoReason
550 (hang (text "Multiple INLINE pragmas for" <+> ppr poly_id)
551 2 (vcat (text "Ignoring all but the first"
552 : map pp_inl (inl1:inl2:inls))))
553
554 pp_inl (L loc prag) = ppr prag <+> parens (ppr loc)
555
556
557 {- *********************************************************************
558 * *
559 SPECIALISE pragmas
560 * *
561 ************************************************************************
562
563 Note [Handling SPECIALISE pragmas]
564 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
565 The basic idea is this:
566
567 foo :: Num a => a -> b -> a
568 {-# SPECIALISE foo :: Int -> b -> Int #-}
569
570 We check that
571 (forall a b. Num a => a -> b -> a)
572 is more polymorphic than
573 forall b. Int -> b -> Int
574 (for which we could use tcSubType, but see below), generating a HsWrapper
575 to connect the two, something like
576 wrap = /\b. <hole> Int b dNumInt
577 This wrapper is put in the TcSpecPrag, in the ABExport record of
578 the AbsBinds.
579
580
581 f :: (Eq a, Ix b) => a -> b -> Bool
582 {-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-}
583 f = <poly_rhs>
584
585 From this the typechecker generates
586
587 AbsBinds [ab] [d1,d2] [([ab], f, f_mono, prags)] binds
588
589 SpecPrag (wrap_fn :: forall a b. (Eq a, Ix b) => XXX
590 -> forall p q. (Ix p, Ix q) => XXX[ Int/a, (p,q)/b ])
591
592 From these we generate:
593
594 Rule: forall p, q, (dp:Ix p), (dq:Ix q).
595 f Int (p,q) dInt ($dfInPair dp dq) = f_spec p q dp dq
596
597 Spec bind: f_spec = wrap_fn <poly_rhs>
598
599 Note that
600
601 * The LHS of the rule may mention dictionary *expressions* (eg
602 $dfIxPair dp dq), and that is essential because the dp, dq are
603 needed on the RHS.
604
605 * The RHS of f_spec, <poly_rhs> has a *copy* of 'binds', so that it
606 can fully specialise it.
607
608
609
610 From the TcSpecPrag, in DsBinds we generate a binding for f_spec and a RULE:
611
612 f_spec :: Int -> b -> Int
613 f_spec = wrap<f rhs>
614
615 RULE: forall b (d:Num b). f b d = f_spec b
616
617 The RULE is generated by taking apart the HsWrapper, which is a little
618 delicate, but works.
619
620 Some wrinkles
621
622 1. We don't use full-on tcSubType, because that does co and contra
623 variance and that in turn will generate too complex a LHS for the
624 RULE. So we use a single invocation of skolemise /
625 topInstantiate in tcSpecWrapper. (Actually I think that even
626 the "deeply" stuff may be too much, because it introduces lambdas,
627 though I think it can be made to work without too much trouble.)
628
629 2. We need to take care with type families (Trac #5821). Consider
630 type instance F Int = Bool
631 f :: Num a => a -> F a
632 {-# SPECIALISE foo :: Int -> Bool #-}
633
634 We *could* try to generate an f_spec with precisely the declared type:
635 f_spec :: Int -> Bool
636 f_spec = <f rhs> Int dNumInt |> co
637
638 RULE: forall d. f Int d = f_spec |> sym co
639
640 but the 'co' and 'sym co' are (a) playing no useful role, and (b) are
641 hard to generate. At all costs we must avoid this:
642 RULE: forall d. f Int d |> co = f_spec
643 because the LHS will never match (indeed it's rejected in
644 decomposeRuleLhs).
645
646 So we simply do this:
647 - Generate a constraint to check that the specialised type (after
648 skolemiseation) is equal to the instantiated function type.
649 - But *discard* the evidence (coercion) for that constraint,
650 so that we ultimately generate the simpler code
651 f_spec :: Int -> F Int
652 f_spec = <f rhs> Int dNumInt
653
654 RULE: forall d. f Int d = f_spec
655 You can see this discarding happening in
656
657 3. Note that the HsWrapper can transform *any* function with the right
658 type prefix
659 forall ab. (Eq a, Ix b) => XXX
660 regardless of XXX. It's sort of polymorphic in XXX. This is
661 useful: we use the same wrapper to transform each of the class ops, as
662 well as the dict. That's what goes on in TcInstDcls.mk_meth_spec_prags
663 -}
664
665 tcSpecPrags :: Id -> [LSig GhcRn]
666 -> TcM [LTcSpecPrag]
667 -- Add INLINE and SPECIALSE pragmas
668 -- INLINE prags are added to the (polymorphic) Id directly
669 -- SPECIALISE prags are passed to the desugarer via TcSpecPrags
670 -- Pre-condition: the poly_id is zonked
671 -- Reason: required by tcSubExp
672 tcSpecPrags poly_id prag_sigs
673 = do { traceTc "tcSpecPrags" (ppr poly_id <+> ppr spec_sigs)
674 ; unless (null bad_sigs) warn_discarded_sigs
675 ; pss <- mapAndRecoverM (wrapLocM (tcSpecPrag poly_id)) spec_sigs
676 ; return $ concatMap (\(L l ps) -> map (L l) ps) pss }
677 where
678 spec_sigs = filter isSpecLSig prag_sigs
679 bad_sigs = filter is_bad_sig prag_sigs
680 is_bad_sig s = not (isSpecLSig s || isInlineLSig s || isSCCFunSig s)
681
682 warn_discarded_sigs
683 = addWarnTc NoReason
684 (hang (text "Discarding unexpected pragmas for" <+> ppr poly_id)
685 2 (vcat (map (ppr . getLoc) bad_sigs)))
686
687 --------------
688 tcSpecPrag :: TcId -> Sig GhcRn -> TcM [TcSpecPrag]
689 tcSpecPrag poly_id prag@(SpecSig fun_name hs_tys inl)
690 -- See Note [Handling SPECIALISE pragmas]
691 --
692 -- The Name fun_name in the SpecSig may not be the same as that of the poly_id
693 -- Example: SPECIALISE for a class method: the Name in the SpecSig is
694 -- for the selector Id, but the poly_id is something like $cop
695 -- However we want to use fun_name in the error message, since that is
696 -- what the user wrote (Trac #8537)
697 = addErrCtxt (spec_ctxt prag) $
698 do { warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl))
699 (text "SPECIALISE pragma for non-overloaded function"
700 <+> quotes (ppr fun_name))
701 -- Note [SPECIALISE pragmas]
702 ; spec_prags <- mapM tc_one hs_tys
703 ; traceTc "tcSpecPrag" (ppr poly_id $$ nest 2 (vcat (map ppr spec_prags)))
704 ; return spec_prags }
705 where
706 name = idName poly_id
707 poly_ty = idType poly_id
708 spec_ctxt prag = hang (text "In the SPECIALISE pragma") 2 (ppr prag)
709
710 tc_one hs_ty
711 = do { spec_ty <- tcHsSigType (FunSigCtxt name False) hs_ty
712 ; wrap <- tcSpecWrapper (FunSigCtxt name True) poly_ty spec_ty
713 ; return (SpecPrag poly_id wrap inl) }
714
715 tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
716
717 --------------
718 tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
719 -- A simpler variant of tcSubType, used for SPECIALISE pragmas
720 -- See Note [Handling SPECIALISE pragmas], wrinkle 1
721 tcSpecWrapper ctxt poly_ty spec_ty
722 = do { (sk_wrap, inst_wrap)
723 <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
724 do { (inst_wrap, tau) <- topInstantiate orig poly_ty
725 ; _ <- unifyType Nothing spec_tau tau
726 -- Deliberately ignore the evidence
727 -- See Note [Handling SPECIALISE pragmas],
728 -- wrinkle (2)
729 ; return inst_wrap }
730 ; return (sk_wrap <.> inst_wrap) }
731 where
732 orig = SpecPragOrigin ctxt
733
734 --------------
735 tcImpPrags :: [LSig GhcRn] -> TcM [LTcSpecPrag]
736 -- SPECIALISE pragmas for imported things
737 tcImpPrags prags
738 = do { this_mod <- getModule
739 ; dflags <- getDynFlags
740 ; if (not_specialising dflags) then
741 return []
742 else do
743 { pss <- mapAndRecoverM (wrapLocM tcImpSpec)
744 [L loc (name,prag)
745 | (L loc prag@(SpecSig (L _ name) _ _)) <- prags
746 , not (nameIsLocalOrFrom this_mod name) ]
747 ; return $ concatMap (\(L l ps) -> map (L l) ps) pss } }
748 where
749 -- Ignore SPECIALISE pragmas for imported things
750 -- when we aren't specialising, or when we aren't generating
751 -- code. The latter happens when Haddocking the base library;
752 -- we don't want complaints about lack of INLINABLE pragmas
753 not_specialising dflags
754 | not (gopt Opt_Specialise dflags) = True
755 | otherwise = case hscTarget dflags of
756 HscNothing -> True
757 HscInterpreted -> True
758 _other -> False
759
760 tcImpSpec :: (Name, Sig GhcRn) -> TcM [TcSpecPrag]
761 tcImpSpec (name, prag)
762 = do { id <- tcLookupId name
763 ; unless (isAnyInlinePragma (idInlinePragma id))
764 (addWarnTc NoReason (impSpecErr name))
765 ; tcSpecPrag id prag }
766
767 impSpecErr :: Name -> SDoc
768 impSpecErr name
769 = hang (text "You cannot SPECIALISE" <+> quotes (ppr name))
770 2 (vcat [ text "because its definition has no INLINE/INLINABLE pragma"
771 , parens $ sep
772 [ text "or its defining module" <+> quotes (ppr mod)
773 , text "was compiled without -O"]])
774 where
775 mod = nameModule name