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