summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Gen/Sig.hs
blob: 35f6951ae13fbfb407d9ca227c747c6421f8899d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
{-
(c) The University of Glasgow 2006-2012
(c) The GRASP Project, Glasgow University, 1992-2002

-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}

module GHC.Tc.Gen.Sig(
       TcSigInfo(..),
       TcIdSigInfo(..), TcIdSigInst,
       TcPatSynInfo(..),
       TcSigFun,

       isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
       completeSigPolyId_maybe,

       tcTySigs, tcUserTypeSig, completeSigFromId,
       tcInstSig,

       TcPragEnv, emptyPragEnv, lookupPragEnv, extendPragEnv,
       mkPragEnv, tcSpecPrags, tcSpecWrapper, tcImpPrags, addInlinePrags
   ) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.Hs
import GHC.Tc.Gen.HsType
import GHC.Tc.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
import GHC.Tc.Utils.Env( tcLookupId )
import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
import GHC.Core.Type ( mkTyVarBinders )
import GHC.Core.Multiplicity

import GHC.Driver.Session
import GHC.Driver.Backend
import GHC.Types.Var ( TyVar, Specificity(..), tyVarKind, binderVars )
import GHC.Types.Id  ( Id, idName, idType, idInlinePragma, setInlinePragma, mkLocalId )
import GHC.Builtin.Names( mkUnboundName )
import GHC.Types.Basic
import GHC.Unit.Module( getModule )
import GHC.Types.Name
import GHC.Types.Name.Env
import GHC.Utils.Outputable
import GHC.Types.SrcLoc
import GHC.Utils.Misc( singleton )
import GHC.Data.Maybe( orElse )
import Data.Maybe( mapMaybe )
import Control.Monad( unless )


{- -------------------------------------------------------------
          Note [Overview of type signatures]
----------------------------------------------------------------
Type signatures, including partial signatures, are jolly tricky,
especially on value bindings.  Here's an overview.

    f :: forall a. [a] -> [a]
    g :: forall b. _ -> b

    f = ...g...
    g = ...f...

* HsSyn: a signature in a binding starts off as a TypeSig, in
  type HsBinds.Sig

* When starting a mutually recursive group, like f/g above, we
  call tcTySig on each signature in the group.

* tcTySig: Sig -> TcIdSigInfo
  - For a /complete/ signature, like 'f' above, tcTySig kind-checks
    the HsType, producing a Type, and wraps it in a CompleteSig, and
    extend the type environment with this polymorphic 'f'.

  - For a /partial/signature, like 'g' above, tcTySig does nothing
    Instead it just wraps the pieces in a PartialSig, to be handled
    later.

* tcInstSig: TcIdSigInfo -> TcIdSigInst
  In tcMonoBinds, when looking at an individual binding, we use
  tcInstSig to instantiate the signature forall's in the signature,
  and attribute that instantiated (monomorphic) type to the
  binder.  You can see this in GHC.Tc.Gen.Bind.tcLhsId.

  The instantiation does the obvious thing for complete signatures,
  but for /partial/ signatures it starts from the HsSyn, so it
  has to kind-check it etc: tcHsPartialSigType.  It's convenient
  to do this at the same time as instantiation, because we can
  make the wildcards into unification variables right away, raather
  than somehow quantifying over them.  And the "TcLevel" of those
  unification variables is correct because we are in tcMonoBinds.


Note [Scoped tyvars]
~~~~~~~~~~~~~~~~~~~~
The -XScopedTypeVariables flag brings lexically-scoped type variables
into scope for any explicitly forall-quantified type variables:
        f :: forall a. a -> a
        f x = e
Then 'a' is in scope inside 'e'.

However, we do *not* support this
  - For pattern bindings e.g
        f :: forall a. a->a
        (f,g) = e

Note [Binding scoped type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type variables *brought into lexical scope* by a type signature
may be a subset of the *quantified type variables* of the signatures,
for two reasons:

* With kind polymorphism a signature like
    f :: forall f a. f a -> f a
  may actually give rise to
    f :: forall k. forall (f::k -> *) (a:k). f a -> f a
  So the sig_tvs will be [k,f,a], but only f,a are scoped.
  NB: the scoped ones are not necessarily the *initial* ones!

* Even aside from kind polymorphism, there may be more instantiated
  type variables than lexically-scoped ones.  For example:
        type T a = forall b. b -> (a,b)
        f :: forall c. T c
  Here, the signature for f will have one scoped type variable, c,
  but two instantiated type variables, c' and b'.

However, all of this only applies to the renamer.  The typechecker
just puts all of them into the type environment; any lexical-scope
errors were dealt with by the renamer.

-}


{- *********************************************************************
*                                                                      *
             Utility functions for TcSigInfo
*                                                                      *
********************************************************************* -}

tcIdSigName :: TcIdSigInfo -> Name
tcIdSigName (CompleteSig { sig_bndr = id }) = idName id
tcIdSigName (PartialSig { psig_name = n })  = n

tcSigInfoName :: TcSigInfo -> Name
tcSigInfoName (TcIdSig     idsi) = tcIdSigName idsi
tcSigInfoName (TcPatSynSig tpsi) = patsig_name tpsi

completeSigPolyId_maybe :: TcSigInfo -> Maybe TcId
completeSigPolyId_maybe sig
  | TcIdSig sig_info <- sig
  , CompleteSig { sig_bndr = id } <- sig_info = Just id
  | otherwise                                 = Nothing


{- *********************************************************************
*                                                                      *
               Typechecking user signatures
*                                                                      *
********************************************************************* -}

tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
tcTySigs hs_sigs
  = checkNoErrs $
    do { -- Fail if any of the signatures is duff
         -- Hence mapAndReportM
         -- See Note [Fail eagerly on bad signatures]
         ty_sigs_s <- mapAndReportM tcTySig hs_sigs

       ; let ty_sigs = concat ty_sigs_s
             poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs
                        -- The returned [TcId] are the ones for which we have
                        -- a complete type signature.
                        -- See Note [Complete and partial type signatures]
             env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]

       ; return (poly_ids, lookupNameEnv env) }

tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
tcTySig (L _ (IdSig _ id))
  = do { let ctxt = FunSigCtxt (idName id) False
                    -- False: do not report redundant constraints
                    -- The user has no control over the signature!
             sig = completeSigFromId ctxt id
       ; return [TcIdSig sig] }

tcTySig (L loc (TypeSig _ names sig_ty))
  = setSrcSpan loc $
    do { sigs <- sequence [ tcUserTypeSig loc sig_ty (Just name)
                          | L _ name <- names ]
       ; return (map TcIdSig sigs) }

tcTySig (L loc (PatSynSig _ names sig_ty))
  = setSrcSpan loc $
    do { tpsigs <- sequence [ tcPatSynSig name sig_ty
                            | L _ name <- names ]
       ; return (map TcPatSynSig tpsigs) }

tcTySig _ = return []


tcUserTypeSig :: SrcSpan -> LHsSigWcType GhcRn -> Maybe Name
              -> TcM TcIdSigInfo
-- A function or expression type signature
-- Returns a fully quantified type signature; even the wildcards
-- are quantified with ordinary skolems that should be instantiated
--
-- The SrcSpan is what to declare as the binding site of the
-- any skolems in the signature. For function signatures we
-- use the whole `f :: ty' signature; for expression signatures
-- just the type part.
--
-- Just n  => Function type signature       name :: type
-- Nothing => Expression type signature   <expr> :: type
tcUserTypeSig loc hs_sig_ty mb_name
  | isCompleteHsSig hs_sig_ty
  = do { sigma_ty <- tcHsSigWcType ctxt_F hs_sig_ty
       ; traceTc "tcuser" (ppr sigma_ty)
       ; return $
         CompleteSig { sig_bndr  = mkLocalId name Many sigma_ty
                                   -- We use `Many' as the multiplicity here,
                                   -- as if this identifier corresponds to
                                   -- anything, it is a top-level
                                   -- definition. Which are all unrestricted in
                                   -- the current implementation.
                     , sig_ctxt  = ctxt_T
                     , sig_loc   = loc } }
                       -- Location of the <type> in   f :: <type>

  -- Partial sig with wildcards
  | otherwise
  = return (PartialSig { psig_name = name, psig_hs_ty = hs_sig_ty
                       , sig_ctxt = ctxt_F, sig_loc = loc })
  where
    name   = case mb_name of
               Just n  -> n
               Nothing -> mkUnboundName (mkVarOcc "<expression>")
    ctxt_F = case mb_name of
               Just n  -> FunSigCtxt n False
               Nothing -> ExprSigCtxt
    ctxt_T = case mb_name of
               Just n  -> FunSigCtxt n True
               Nothing -> ExprSigCtxt



completeSigFromId :: UserTypeCtxt -> Id -> TcIdSigInfo
-- Used for instance methods and record selectors
completeSigFromId ctxt id
  = CompleteSig { sig_bndr = id
                , sig_ctxt = ctxt
                , sig_loc  = getSrcSpan id }

isCompleteHsSig :: LHsSigWcType GhcRn -> Bool
-- ^ If there are no wildcards, return a LHsSigType
isCompleteHsSig (HsWC { hswc_ext  = wcs
                      , hswc_body = HsIB { hsib_body = hs_ty } })
   = null wcs && no_anon_wc hs_ty

no_anon_wc :: LHsType GhcRn -> Bool
no_anon_wc lty = go lty
  where
    go (L _ ty) = case ty of
      HsWildCardTy _                 -> False
      HsAppTy _ ty1 ty2              -> go ty1 && go ty2
      HsAppKindTy _ ty ki            -> go ty && go ki
      HsFunTy _ w ty1 ty2            -> go ty1 && go ty2 && go (arrowToHsType w)
      HsListTy _ ty                  -> go ty
      HsTupleTy _ _ tys              -> gos tys
      HsSumTy _ tys                  -> gos tys
      HsOpTy _ ty1 _ ty2             -> go ty1 && go ty2
      HsParTy _ ty                   -> go ty
      HsIParamTy _ _ ty              -> go ty
      HsKindSig _ ty kind            -> go ty && go kind
      HsDocTy _ ty _                 -> go ty
      HsBangTy _ _ ty                -> go ty
      HsRecTy _ flds                 -> gos $ map (cd_fld_type . unLoc) flds
      HsExplicitListTy _ _ tys       -> gos tys
      HsExplicitTupleTy _ tys        -> gos tys
      HsForAllTy { hst_tele = tele
                 , hst_body = ty } -> no_anon_wc_tele tele
                                        && go ty
      HsQualTy { hst_ctxt = L _ ctxt
               , hst_body = ty }  -> gos ctxt && go ty
      HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)) -> go $ L noSrcSpan ty
      HsSpliceTy{} -> True
      HsTyLit{} -> True
      HsTyVar{} -> True
      HsStarTy{} -> True
      XHsType (NHsCoreTy{}) -> True      -- Core type, which does not have any wildcard

    gos = all go

no_anon_wc_tele :: HsForAllTelescope GhcRn -> Bool
no_anon_wc_tele tele = case tele of
  HsForAllVis   { hsf_vis_bndrs   = ltvs } -> all (go . unLoc) ltvs
  HsForAllInvis { hsf_invis_bndrs = ltvs } -> all (go . unLoc) ltvs
  where
    go (UserTyVar _ _ _)      = True
    go (KindedTyVar _ _ _ ki) = no_anon_wc ki

{- Note [Fail eagerly on bad signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If a type signature is wrong, fail immediately:

 * the type sigs may bind type variables, so proceeding without them
   can lead to a cascade of errors

 * the type signature might be ambiguous, in which case checking
   the code against the signature will give a very similar error
   to the ambiguity error.

ToDo: this means we fall over if any top-level type signature in the
module is wrong, because we typecheck all the signatures together
(see GHC.Tc.Gen.Bind.tcValBinds).  Moreover, because of top-level
captureTopConstraints, only insoluble constraints will be reported.
We typecheck all signatures at the same time because a signature
like   f,g :: blah   might have f and g from different SCCs.

So it's a bit awkward to get better error recovery, and no one
has complained!
-}

{- *********************************************************************
*                                                                      *
        Type checking a pattern synonym signature
*                                                                      *
************************************************************************

Note [Pattern synonym signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Pattern synonym signatures are surprisingly tricky (see #11224 for example).
In general they look like this:

   pattern P :: forall univ_tvs. req_theta
             => forall ex_tvs. prov_theta
             => arg1 -> .. -> argn -> res_ty

For parsing and renaming we treat the signature as an ordinary LHsSigType.

Once we get to type checking, we decompose it into its parts, in tcPatSynSig.

* Note that 'forall univ_tvs' and 'req_theta =>'
        and 'forall ex_tvs'   and 'prov_theta =>'
  are all optional.  We gather the pieces at the top of tcPatSynSig

* Initially the implicitly-bound tyvars (added by the renamer) include both
  universal and existential vars.

* After we kind-check the pieces and convert to Types, we do kind generalisation.

Note [solveEqualities in tcPatSynSig]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's important that we solve /all/ the equalities in a pattern
synonym signature, because we are going to zonk the signature to
a Type (not a TcType), in GHC.Tc.TyCl.PatSyn.tc_patsyn_finish, and that
fails if there are un-filled-in coercion variables mentioned
in the type (#15694).

The best thing is simply to use solveEqualities to solve all the
equalites, rather than leaving them in the ambient constraints
to be solved later.  Pattern synonyms are top-level, so there's
no problem with completely solving them.

(NB: this solveEqualities wraps newImplicitTKBndrs, which itself
does a solveLocalEqualities; so solveEqualities isn't going to
make any further progress; it'll just report any unsolved ones,
and fail, as it should.)
-}

tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
-- See Note [Pattern synonym signatures]
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
tcPatSynSig name sig_ty
  | HsIB { hsib_ext = implicit_hs_tvs
         , hsib_body = hs_ty }  <- sig_ty
  , (univ_hs_tvbndrs, hs_req,  hs_ty1)     <- splitLHsSigmaTyInvis hs_ty
  , (ex_hs_tvbndrs,   hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
  = do {  traceTc "tcPatSynSig 1" (ppr sig_ty)
       ; (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty))))
           <- pushTcLevelM_   $
              solveEqualities $ -- See Note [solveEqualities in tcPatSynSig]
              bindImplicitTKBndrs_Skol implicit_hs_tvs $
              bindExplicitTKBndrs_Skol univ_hs_tvbndrs $
              bindExplicitTKBndrs_Skol ex_hs_tvbndrs   $
              do { req     <- tcHsContext hs_req
                 ; prov    <- tcHsContext hs_prov
                 ; body_ty <- tcHsOpenType hs_body_ty
                     -- A (literal) pattern can be unlifted;
                     -- e.g. pattern Zero <- 0#   (#12094)
                 ; return (req, prov, body_ty) }

       ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvbndrs
                                                 req ex_tvbndrs prov body_ty

       -- Kind generalisation
       ; kvs <- kindGeneralizeAll ungen_patsyn_ty
       ; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)

       -- These are /signatures/ so we zonk to squeeze out any kind
       -- unification variables.  Do this after kindGeneralize which may
       -- default kind variables to *.
       ; implicit_tvs <- zonkAndScopedSort implicit_tvs
       ; univ_tvbndrs <- mapM zonkTyCoVarKindBinder univ_tvbndrs
       ; ex_tvbndrs   <- mapM zonkTyCoVarKindBinder ex_tvbndrs
       ; req          <- zonkTcTypes req
       ; prov         <- zonkTcTypes prov
       ; body_ty      <- zonkTcType  body_ty

       -- Skolems have TcLevels too, though they're used only for debugging.
       -- If you don't do this, the debugging checks fail in GHC.Tc.TyCl.PatSyn.
       -- Test case: patsyn/should_compile/T13441
{-
       ; tclvl <- getTcLevel
       ; let env0                  = mkEmptyTCvSubst $ mkInScopeSet $ mkVarSet kvs
             (env1, implicit_tvs') = promoteSkolemsX tclvl env0 implicit_tvs
             (env2, univ_tvs')     = promoteSkolemsX tclvl env1 univ_tvs
             (env3, ex_tvs')       = promoteSkolemsX tclvl env2 ex_tvs
             req'                  = substTys env3 req
             prov'                 = substTys env3 prov
             body_ty'              = substTy  env3 body_ty
-}
      ; let implicit_tvs' = implicit_tvs
            univ_tvbndrs' = univ_tvbndrs
            ex_tvbndrs'   = ex_tvbndrs
            req'          = req
            prov'         = prov
            body_ty'      = body_ty

       -- Now do validity checking
       ; checkValidType ctxt $
         build_patsyn_type kvs implicit_tvs' univ_tvbndrs' req' ex_tvbndrs' prov' body_ty'

       -- arguments become the types of binders. We thus cannot allow
       -- levity polymorphism here
       ; let (arg_tys, _) = tcSplitFunTys body_ty'
       ; mapM_ (checkForLevPoly empty . scaledThing) arg_tys

       ; traceTc "tcTySig }" $
         vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs'
              , text "kvs" <+> ppr_tvs kvs
              , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs')
              , text "req" <+> ppr req'
              , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs')
              , text "prov" <+> ppr prov'
              , text "body_ty" <+> ppr body_ty' ]
       ; return (TPSI { patsig_name = name
                      , patsig_implicit_bndrs = mkTyVarBinders InferredSpec kvs ++
                                                mkTyVarBinders SpecifiedSpec implicit_tvs'
                      , patsig_univ_bndrs     = univ_tvbndrs'
                      , patsig_req            = req'
                      , patsig_ex_bndrs       = ex_tvbndrs'
                      , patsig_prov           = prov'
                      , patsig_body_ty        = body_ty' }) }
  where
    ctxt = PatSynCtxt name

    build_patsyn_type kvs imp univ_bndrs req ex_bndrs prov body
      = mkInfForAllTys kvs $
        mkSpecForAllTys imp $
        mkInvisForAllTys univ_bndrs $
        mkPhiTy req $
        mkInvisForAllTys ex_bndrs $
        mkPhiTy prov $
        body

ppr_tvs :: [TyVar] -> SDoc
ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
                           | tv <- tvs])


{- *********************************************************************
*                                                                      *
               Instantiating user signatures
*                                                                      *
********************************************************************* -}


tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
-- Instantiate a type signature; only used with plan InferGen
tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
  = setSrcSpan loc $  -- Set the binding site of the tyvars
    do { (tv_prs, theta, tau) <- tcInstTypeBndrs poly_id
              -- See Note [Pattern bindings and complete signatures]

       ; return (TISI { sig_inst_sig   = sig
                      , sig_inst_skols = tv_prs
                      , sig_inst_wcs   = []
                      , sig_inst_wcx   = Nothing
                      , sig_inst_theta = theta
                      , sig_inst_tau   = tau }) }

tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty
                             , sig_ctxt = ctxt
                             , sig_loc = loc })
  = setSrcSpan loc $  -- Set the binding site of the tyvars
    do { traceTc "Staring partial sig {" (ppr hs_sig)
       ; (wcs, wcx, tv_prs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
         -- See Note [Checking partial type signatures] in GHC.Tc.Gen.HsType
       ; let inst_sig = TISI { sig_inst_sig   = hs_sig
                             , sig_inst_skols = tv_prs
                             , sig_inst_wcs   = wcs
                             , sig_inst_wcx   = wcx
                             , sig_inst_theta = theta
                             , sig_inst_tau   = tau }
       ; traceTc "End partial sig }" (ppr inst_sig)
       ; return inst_sig }


{- Note [Pattern bindings and complete signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
      data T a = MkT a a
      f :: forall a. a->a
      g :: forall b. b->b
      MkT f g = MkT (\x->x) (\y->y)
Here we'll infer a type from the pattern of 'T a', but if we feed in
the signature types for f and g, we'll end up unifying 'a' and 'b'

So we instantiate f and g's signature with TyVarTv skolems
(newMetaTyVarTyVars) that can unify with each other.  If too much
unification takes place, we'll find out when we do the final
impedance-matching check in GHC.Tc.Gen.Bind.mkExport

See Note [Signature skolems] in GHC.Tc.Utils.TcType

None of this applies to a function binding with a complete
signature, which doesn't use tcInstSig.  See GHC.Tc.Gen.Bind.tcPolyCheck.
-}

{- *********************************************************************
*                                                                      *
                   Pragmas and PragEnv
*                                                                      *
********************************************************************* -}

type TcPragEnv = NameEnv [LSig GhcRn]

emptyPragEnv :: TcPragEnv
emptyPragEnv = emptyNameEnv

lookupPragEnv :: TcPragEnv -> Name -> [LSig GhcRn]
lookupPragEnv prag_fn n = lookupNameEnv prag_fn n `orElse` []

extendPragEnv :: TcPragEnv -> (Name, LSig GhcRn) -> TcPragEnv
extendPragEnv prag_fn (n, sig) = extendNameEnv_Acc (:) singleton prag_fn n sig

---------------
mkPragEnv :: [LSig GhcRn] -> LHsBinds GhcRn -> TcPragEnv
mkPragEnv sigs binds
  = foldl' extendPragEnv emptyNameEnv prs
  where
    prs = mapMaybe get_sig sigs

    get_sig :: LSig GhcRn -> Maybe (Name, LSig GhcRn)
    get_sig (L l (SpecSig x lnm@(L _ nm) ty inl))
      = Just (nm, L l $ SpecSig   x lnm ty (add_arity nm inl))
    get_sig (L l (InlineSig x lnm@(L _ nm) inl))
      = Just (nm, L l $ InlineSig x lnm    (add_arity nm inl))
    get_sig (L l (SCCFunSig x st lnm@(L _ nm) str))
      = Just (nm, L l $ SCCFunSig x st lnm str)
    get_sig _ = Nothing

    add_arity n inl_prag   -- Adjust inl_sat field to match visible arity of function
      | Inline <- inl_inline inl_prag
        -- add arity only for real INLINE pragmas, not INLINABLE
      = case lookupNameEnv ar_env n of
          Just ar -> inl_prag { inl_sat = Just ar }
          Nothing -> WARN( True, text "mkPragEnv no arity" <+> ppr n )
                     -- There really should be a binding for every INLINE pragma
                     inl_prag
      | otherwise
      = inl_prag

    -- ar_env maps a local to the arity of its definition
    ar_env :: NameEnv Arity
    ar_env = foldr lhsBindArity emptyNameEnv binds

lhsBindArity :: LHsBind GhcRn -> NameEnv Arity -> NameEnv Arity
lhsBindArity (L _ (FunBind { fun_id = id, fun_matches = ms })) env
  = extendNameEnv env (unLoc id) (matchGroupArity ms)
lhsBindArity _ env = env        -- PatBind/VarBind


-----------------
addInlinePrags :: TcId -> [LSig GhcRn] -> TcM TcId
addInlinePrags poly_id prags_for_me
  | inl@(L _ prag) : inls <- inl_prags
  = do { traceTc "addInlinePrag" (ppr poly_id $$ ppr prag)
       ; unless (null inls) (warn_multiple_inlines inl inls)
       ; return (poly_id `setInlinePragma` prag) }
  | otherwise
  = return poly_id
  where
    inl_prags = [L loc prag | L loc (InlineSig _ _ prag) <- prags_for_me]

    warn_multiple_inlines _ [] = return ()

    warn_multiple_inlines inl1@(L loc prag1) (inl2@(L _ prag2) : inls)
       | inlinePragmaActivation prag1 == inlinePragmaActivation prag2
       , noUserInlineSpec (inlinePragmaSpec prag1)
       =    -- Tiresome: inl1 is put there by virtue of being in a hs-boot loop
            -- and inl2 is a user NOINLINE pragma; we don't want to complain
         warn_multiple_inlines inl2 inls
       | otherwise
       = setSrcSpan loc $
         addWarnTc NoReason
                     (hang (text "Multiple INLINE pragmas for" <+> ppr poly_id)
                       2 (vcat (text "Ignoring all but the first"
                                : map pp_inl (inl1:inl2:inls))))

    pp_inl (L loc prag) = ppr prag <+> parens (ppr loc)


{- *********************************************************************
*                                                                      *
                   SPECIALISE pragmas
*                                                                      *
************************************************************************

Note [Handling SPECIALISE pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The basic idea is this:

   foo :: Num a => a -> b -> a
   {-# SPECIALISE foo :: Int -> b -> Int #-}

We check that
   (forall a b. Num a => a -> b -> a)
      is more polymorphic than
   forall b. Int -> b -> Int
(for which we could use tcSubType, but see below), generating a HsWrapper
to connect the two, something like
      wrap = /\b. <hole> Int b dNumInt
This wrapper is put in the TcSpecPrag, in the ABExport record of
the AbsBinds.


        f :: (Eq a, Ix b) => a -> b -> Bool
        {-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-}
        f = <poly_rhs>

From this the typechecker generates

    AbsBinds [ab] [d1,d2] [([ab], f, f_mono, prags)] binds

    SpecPrag (wrap_fn :: forall a b. (Eq a, Ix b) => XXX
                      -> forall p q. (Ix p, Ix q) => XXX[ Int/a, (p,q)/b ])

From these we generate:

    Rule:       forall p, q, (dp:Ix p), (dq:Ix q).
                    f Int (p,q) dInt ($dfInPair dp dq) = f_spec p q dp dq

    Spec bind:  f_spec = wrap_fn <poly_rhs>

Note that

  * The LHS of the rule may mention dictionary *expressions* (eg
    $dfIxPair dp dq), and that is essential because the dp, dq are
    needed on the RHS.

  * The RHS of f_spec, <poly_rhs> has a *copy* of 'binds', so that it
    can fully specialise it.

From the TcSpecPrag, in GHC.HsToCore.Binds we generate a binding for f_spec and a RULE:

   f_spec :: Int -> b -> Int
   f_spec = wrap<f rhs>

   RULE: forall b (d:Num b). f b d = f_spec b

The RULE is generated by taking apart the HsWrapper, which is a little
delicate, but works.

Some wrinkles

1. In tcSpecWrapper, rather than calling tcSubType, we directly call
   skolemise/instantiate.  That is mainly because of wrinkle (2).

   Historical note: in the past, tcSubType did co/contra stuff, which
   could generate too complex a LHS for the RULE, which was another
   reason for not using tcSubType.  But that reason has gone away
   with simple subsumption (#17775).

2. We need to take care with type families (#5821).  Consider
      type instance F Int = Bool
      f :: Num a => a -> F a
      {-# SPECIALISE foo :: Int -> Bool #-}

  We *could* try to generate an f_spec with precisely the declared type:
      f_spec :: Int -> Bool
      f_spec = <f rhs> Int dNumInt |> co

      RULE: forall d. f Int d = f_spec |> sym co

  but the 'co' and 'sym co' are (a) playing no useful role, and (b) are
  hard to generate.  At all costs we must avoid this:
      RULE: forall d. f Int d |> co = f_spec
  because the LHS will never match (indeed it's rejected in
  decomposeRuleLhs).

  So we simply do this:
    - Generate a constraint to check that the specialised type (after
      skolemisation) is equal to the instantiated function type.
    - But *discard* the evidence (coercion) for that constraint,
      so that we ultimately generate the simpler code
          f_spec :: Int -> F Int
          f_spec = <f rhs> Int dNumInt

          RULE: forall d. f Int d = f_spec
      You can see this discarding happening in tcSpecPrag

3. Note that the HsWrapper can transform *any* function with the right
   type prefix
       forall ab. (Eq a, Ix b) => XXX
   regardless of XXX.  It's sort of polymorphic in XXX.  This is
   useful: we use the same wrapper to transform each of the class ops, as
   well as the dict.  That's what goes on in GHC.Tc.TyCl.Instance.mk_meth_spec_prags
-}

tcSpecPrags :: Id -> [LSig GhcRn]
            -> TcM [LTcSpecPrag]
-- Add INLINE and SPECIALSE pragmas
--    INLINE prags are added to the (polymorphic) Id directly
--    SPECIALISE prags are passed to the desugarer via TcSpecPrags
-- Pre-condition: the poly_id is zonked
-- Reason: required by tcSubExp
tcSpecPrags poly_id prag_sigs
  = do { traceTc "tcSpecPrags" (ppr poly_id <+> ppr spec_sigs)
       ; unless (null bad_sigs) warn_discarded_sigs
       ; pss <- mapAndRecoverM (wrapLocM (tcSpecPrag poly_id)) spec_sigs
       ; return $ concatMap (\(L l ps) -> map (L l) ps) pss }
  where
    spec_sigs = filter isSpecLSig prag_sigs
    bad_sigs  = filter is_bad_sig prag_sigs
    is_bad_sig s = not (isSpecLSig s || isInlineLSig s || isSCCFunSig s)

    warn_discarded_sigs
      = addWarnTc NoReason
                  (hang (text "Discarding unexpected pragmas for" <+> ppr poly_id)
                      2 (vcat (map (ppr . getLoc) bad_sigs)))

--------------
tcSpecPrag :: TcId -> Sig GhcRn -> TcM [TcSpecPrag]
tcSpecPrag poly_id prag@(SpecSig _ fun_name hs_tys inl)
-- See Note [Handling SPECIALISE pragmas]
--
-- The Name fun_name in the SpecSig may not be the same as that of the poly_id
-- Example: SPECIALISE for a class method: the Name in the SpecSig is
--          for the selector Id, but the poly_id is something like $cop
-- However we want to use fun_name in the error message, since that is
-- what the user wrote (#8537)
  = addErrCtxt (spec_ctxt prag) $
    do  { warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl))
                 (text "SPECIALISE pragma for non-overloaded function"
                  <+> quotes (ppr fun_name))
                  -- Note [SPECIALISE pragmas]
        ; spec_prags <- mapM tc_one hs_tys
        ; traceTc "tcSpecPrag" (ppr poly_id $$ nest 2 (vcat (map ppr spec_prags)))
        ; return spec_prags }
  where
    name      = idName poly_id
    poly_ty   = idType poly_id
    spec_ctxt prag = hang (text "In the pragma:") 2 (ppr prag)

    tc_one hs_ty
      = do { spec_ty <- tcHsSigType   (FunSigCtxt name False) hs_ty
           ; wrap    <- tcSpecWrapper (FunSigCtxt name True)  poly_ty spec_ty
           ; return (SpecPrag poly_id wrap inl) }

tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)

--------------
tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- A simpler variant of tcSubType, used for SPECIALISE pragmas
-- See Note [Handling SPECIALISE pragmas], wrinkle 1
tcSpecWrapper ctxt poly_ty spec_ty
  = do { (sk_wrap, inst_wrap)
               <- tcSkolemise ctxt spec_ty $ \ spec_tau ->
                  do { (inst_wrap, tau) <- topInstantiate orig poly_ty
                     ; _ <- unifyType Nothing spec_tau tau
                            -- Deliberately ignore the evidence
                            -- See Note [Handling SPECIALISE pragmas],
                            --   wrinkle (2)
                     ; return inst_wrap }
       ; return (sk_wrap <.> inst_wrap) }
  where
    orig = SpecPragOrigin ctxt

--------------
tcImpPrags :: [LSig GhcRn] -> TcM [LTcSpecPrag]
-- SPECIALISE pragmas for imported things
tcImpPrags prags
  = do { this_mod <- getModule
       ; dflags <- getDynFlags
       ; if (not_specialising dflags) then
            return []
         else do
            { pss <- mapAndRecoverM (wrapLocM tcImpSpec)
                     [L loc (name,prag)
                             | (L loc prag@(SpecSig _ (L _ name) _ _)) <- prags
                             , not (nameIsLocalOrFrom this_mod name) ]
            ; return $ concatMap (\(L l ps) -> map (L l) ps) pss } }
  where
    -- Ignore SPECIALISE pragmas for imported things
    -- when we aren't specialising, or when we aren't generating
    -- code.  The latter happens when Haddocking the base library;
    -- we don't want complaints about lack of INLINABLE pragmas
    not_specialising dflags
      | not (gopt Opt_Specialise dflags) = True
      | otherwise = case backend dflags of
                      NoBackend   -> True
                      Interpreter -> True
                      _other      -> False

tcImpSpec :: (Name, Sig GhcRn) -> TcM [TcSpecPrag]
tcImpSpec (name, prag)
 = do { id <- tcLookupId name
      ; if isAnyInlinePragma (idInlinePragma id)
        then tcSpecPrag id prag
        else do { addWarnTc NoReason (impSpecErr name)
                ; return [] } }
      -- If there is no INLINE/INLINABLE pragma there will be no unfolding. In
      -- that case, just delete the SPECIALISE pragma altogether, lest the
      -- desugarer fall over because it can't find the unfolding. See #18118.

impSpecErr :: Name -> SDoc
impSpecErr name
  = hang (text "You cannot SPECIALISE" <+> quotes (ppr name))
       2 (vcat [ text "because its definition has no INLINE/INLINABLE pragma"
               , parens $ sep
                   [ text "or its defining module" <+> quotes (ppr mod)
                   , text "was compiled without -O"]])
  where
    mod = nameModule name