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