TcInstDcls.hs 74.5 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5 6

TcInstDecls: Typechecking instance declarations
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

11
module TcInstDcls ( tcInstDecls1, tcInstDeclsDeriv, tcInstDecls2 ) where
12

dterei's avatar
dterei committed
13 14
#include "HsVersions.h"

15
import HsSyn
16
import TcBinds
17
import TcTyClsDecls
18
import TcClassDcl( tcClassDecl2, tcATDefault,
19
                   HsSigFun, lookupHsSig, mkHsSigFun,
20
                   findMethodBind, instantiateMethod )
21
import TcSigs
Ian Lynagh's avatar
Ian Lynagh committed
22
import TcRnMonad
23
import TcValidity
24
import TcHsSyn    ( zonkTcTypeToTypes, emptyZonkEnv )
25 26
import TcMType
import TcType
27
import BuildTyCl
28 29 30 31 32 33 34 35
import Inst
import InstEnv
import FamInst
import FamInstEnv
import TcDeriv
import TcEnv
import TcHsType
import TcUnify
36
import CoreSyn    ( Expr(..), mkApps, mkVarApps, mkLams )
dterei's avatar
dterei committed
37
import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
38
import CoreUnfold ( mkInlineUnfolding, mkDFunUnfolding )
39
import Type
40
import TcEvidence
41
import TyCon
42
import CoAxiom
43 44 45
import DataCon
import Class
import Var
46
import VarEnv
47
import VarSet
48
import PrelNames  ( typeableClassName, genericClassNames )
dterei's avatar
dterei committed
49 50 51
import Bag
import BasicTypes
import DynFlags
52
import ErrUtils
dterei's avatar
dterei committed
53
import FastString
54
import Id
55 56 57
import MkId
import Name
import NameSet
dterei's avatar
dterei committed
58
import Outputable
59 60
import SrcLoc
import Util
61
import BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
62
import qualified GHC.LanguageExtensions as LangExt
dterei's avatar
dterei committed
63

64
import Control.Monad
65
import Maybes
66 67


Austin Seipp's avatar
Austin Seipp committed
68
{-
69
Typechecking instance declarations is done in two passes. The first
70 71
pass, made by @tcInstDecls1@, collects information to be used in the
second pass.
72 73 74 75 76 77 78

This pre-processed info includes the as-yet-unprocessed bindings
inside the instance declaration.  These are type-checked in the second
pass, when the class-instance envs and GVE contain all the info from
all the instance and value decls.  Indeed that's the reason we need
two passes over the instance decls.

79 80 81

Note [How instance declarations are translated]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jan Stolarek's avatar
Jan Stolarek committed
82
Here is how we translate instance declarations into Core
83 84

Running example:
dterei's avatar
dterei committed
85 86 87
        class C a where
           op1, op2 :: Ix b => a -> b -> b
           op2 = <dm-rhs>
88

dterei's avatar
dterei committed
89 90 91
        instance C a => C [a]
           {-# INLINE [2] op1 #-}
           op1 = <rhs>
92
===>
dterei's avatar
dterei committed
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
        -- Method selectors
        op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
        op1 = ...
        op2 = ...

        -- Default methods get the 'self' dictionary as argument
        -- so they can call other methods at the same type
        -- Default methods get the same type as their method selector
        $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
        $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
               -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
               -- Note [Tricky type variable scoping]

        -- A top-level definition for each instance method
        -- Here op1_i, op2_i are the "instance method Ids"
        -- The INLINE pragma comes from the user pragma
        {-# INLINE [2] op1_i #-}  -- From the instance decl bindings
        op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
dterei's avatar
dterei committed
111
        op1_i = /\a. \(d:C a).
dterei's avatar
dterei committed
112 113 114 115 116 117 118 119 120 121 122 123
               let this :: C [a]
                   this = df_i a d
                     -- Note [Subtle interaction of recursion and overlap]

                   local_op1 :: forall b. Ix b => [a] -> b -> b
                   local_op1 = <rhs>
                     -- Source code; run the type checker on this
                     -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
                     -- Note [Tricky type variable scoping]

               in local_op1 a d

dterei's avatar
dterei committed
124
        op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
dterei's avatar
dterei committed
125 126 127 128 129 130 131

        -- The dictionary function itself
        {-# NOINLINE CONLIKE df_i #-}   -- Never inline dictionary functions
        df_i :: forall a. C a -> C [a]
        df_i = /\a. \d:C a. MkC (op1_i a d) (op2_i a d)
                -- But see Note [Default methods in instances]
                -- We can't apply the type checker to the default-method call
132

133
        -- Use a RULE to short-circuit applications of the class ops
dterei's avatar
dterei committed
134
        {-# RULE "op1@C[a]" forall a, d:C a.
135 136
                            op1 [a] (df_i d) = op1_i a d #-}

137 138
Note [Instances and loop breakers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
139
* Note that df_i may be mutually recursive with both op1_i and op2_i.
dterei's avatar
dterei committed
140
  It's crucial that df_i is not chosen as the loop breaker, even
141 142 143 144 145 146
  though op1_i has a (user-specified) INLINE pragma.

* Instead the idea is to inline df_i into op1_i, which may then select
  methods from the MkC record, and thereby break the recursion with
  df_i, leaving a *self*-recurisve op1_i.  (If op1_i doesn't call op at
  the same type, it won't mention df_i, so there won't be recursion in
dterei's avatar
dterei committed
147
  the first place.)
148 149 150

* If op1_i is marked INLINE by the user there's a danger that we won't
  inline df_i in it, and that in turn means that (since it'll be a
dterei's avatar
dterei committed
151
  loop-breaker because df_i isn't), op1_i will ironically never be
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
152 153 154 155
  inlined.  But this is OK: the recursion breaking happens by way of
  a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
  unfoldings. See Note [RULEs enabled in SimplGently] in SimplUtils

156 157 158 159 160 161 162 163 164 165
Note [ClassOp/DFun selection]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
One thing we see a lot is stuff like
    op2 (df d1 d2)
where 'op2' is a ClassOp and 'df' is DFun.  Now, we could inline *both*
'op2' and 'df' to get
     case (MkD ($cop1 d1 d2) ($cop2 d1 d2) ... of
       MkD _ op2 _ _ _ -> op2
And that will reduce to ($cop2 d1 d2) which is what we wanted.

dterei's avatar
dterei committed
166
But it's tricky to make this work in practice, because it requires us to
167
inline both 'op2' and 'df'.  But neither is keen to inline without having
dterei's avatar
dterei committed
168
seen the other's result; and it's very easy to get code bloat (from the
169 170 171
big intermediate) if you inline a bit too much.

Instead we use a cunning trick.
dterei's avatar
dterei committed
172
 * We arrange that 'df' and 'op2' NEVER inline.
173 174 175 176 177 178 179 180

 * We arrange that 'df' is ALWAYS defined in the sylised form
      df d1 d2 = MkD ($cop1 d1 d2) ($cop2 d1 d2) ...

 * We give 'df' a magical unfolding (DFunUnfolding [$cop1, $cop2, ..])
   that lists its methods.

 * We make CoreUnfold.exprIsConApp_maybe spot a DFunUnfolding and return
dterei's avatar
dterei committed
181
   a suitable constructor application -- inlining df "on the fly" as it
182 183
   were.

184 185 186
 * ClassOp rules: We give the ClassOp 'op2' a BuiltinRule that
   extracts the right piece iff its argument satisfies
   exprIsConApp_maybe.  This is done in MkId mkDictSelId
187

Gabor Greif's avatar
Gabor Greif committed
188
 * We make 'df' CONLIKE, so that shared uses still match; eg
189 190 191 192 193
      let d = df d1 d2
      in ...(op2 d)...(op1 d)...

Note [Single-method classes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
194
If the class has just one method (or, more accurately, just one element
195
of {superclasses + methods}), then we use a different strategy.
196 197 198 199

   class C a where op :: a -> a
   instance C a => C [a] where op = <blah>

200 201 202
We translate the class decl into a newtype, which just gives a
top-level axiom. The "constructor" MkC expands to a cast, as does the
class-op selector.
203 204 205 206 207 208

   axiom Co:C a :: C a ~ (a->a)

   op :: forall a. C a -> (a -> a)
   op a d = d |> (Co:C a)

209 210 211
   MkC :: forall a. (a->a) -> C a
   MkC = /\a.\op. op |> (sym Co:C a)

212
The clever RULE stuff doesn't work now, because ($df a d) isn't
dterei's avatar
dterei committed
213
a constructor application, so exprIsConApp_maybe won't return
214
Just <blah>.
215

216
Instead, we simply rely on the fact that casts are cheap:
217

218
   $df :: forall a. C a => C [a]
219
   {-# INLINE df #-}  -- NB: INLINE this
220 221
   $df = /\a. \d. MkC [a] ($cop_list a d)
       = $cop_list |> forall a. C a -> (sym (Co:C [a]))
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
222

223 224
   $cop_list :: forall a. C a => [a] -> [a]
   $cop_list = <blah>
225

226 227 228 229
So if we see
   (op ($df a d))
we'll inline 'op' and '$df', since both are simply casts, and
good things happen.
230

231 232 233 234 235
Why do we use this different strategy?  Because otherwise we
end up with non-inlined dictionaries that look like
    $df = $cop |> blah
which adds an extra indirection to every use, which seems stupid.  See
Trac #4138 for an example (although the regression reported there
Simon Peyton Jones's avatar
Simon Peyton Jones committed
236
wasn't due to the indirection).
237

dterei's avatar
dterei committed
238
There is an awkward wrinkle though: we want to be very
239
careful when we have
240 241 242
    instance C a => C [a] where
      {-# INLINE op #-}
      op = ...
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
243 244
then we'll get an INLINE pragma on $cop_list but it's important that
$cop_list only inlines when it's applied to *two* arguments (the
Gabor Greif's avatar
Gabor Greif committed
245
dictionary and the list argument).  So we must not eta-expand $df
dterei's avatar
dterei committed
246
above.  We ensure that this doesn't happen by putting an INLINE
247 248
pragma on the dfun itself; after all, it ends up being just a cast.

dterei's avatar
dterei committed
249
There is one more dark corner to the INLINE story, even more deeply
250 251 252 253 254 255 256
buried.  Consider this (Trac #3772):

    class DeepSeq a => C a where
      gen :: Int -> a

    instance C a => C [a] where
      gen n = ...
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
257

258 259
    class DeepSeq a where
      deepSeq :: a -> b -> b
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
    instance DeepSeq a => DeepSeq [a] where
      {-# INLINE deepSeq #-}
      deepSeq xs b = foldr deepSeq b xs

That gives rise to these defns:

    $cdeepSeq :: DeepSeq a -> [a] -> b -> b
    -- User INLINE( 3 args )!
    $cdeepSeq a (d:DS a) b (x:[a]) (y:b) = ...

    $fDeepSeq[] :: DeepSeq a -> DeepSeq [a]
    -- DFun (with auto INLINE pragma)
    $fDeepSeq[] a d = $cdeepSeq a d |> blah

    $cp1 a d :: C a => DeepSep [a]
    -- We don't want to eta-expand this, lest
    -- $cdeepSeq gets inlined in it!
    $cp1 a d = $fDeepSep[] a (scsel a d)

    $fC[] :: C a => C [a]
    -- Ordinary DFun
    $fC[] a d = MkC ($cp1 a d) ($cgen a d)

Here $cp1 is the code that generates the superclass for C [a].  The
issue is this: we must not eta-expand $cp1 either, or else $fDeepSeq[]
and then $cdeepSeq will inline there, which is definitely wrong.  Like
on the dfun, we solve this by adding an INLINE pragma to $cp1.
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
288

289 290 291 292 293 294 295
Note [Subtle interaction of recursion and overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
  class C a where { op1,op2 :: a -> a }
  instance C a => C [a] where
    op1 x = op2 x ++ op2 x
    op2 x = ...
296
  instance C [Int] where
297 298 299 300 301 302 303
    ...

When type-checking the C [a] instance, we need a C [a] dictionary (for
the call of op2).  If we look up in the instance environment, we find
an overlap.  And in *general* the right thing is to complain (see Note
[Overlapping instances] in InstEnv).  But in *this* case it's wrong to
complain, because we just want to delegate to the op2 of this same
dterei's avatar
dterei committed
304
instance.
305

dterei's avatar
dterei committed
306
Why is this justified?  Because we generate a (C [a]) constraint in
307
a context in which 'a' cannot be instantiated to anything that matches
Gabor Greif's avatar
Gabor Greif committed
308
other overlapping instances, or else we would not be executing this
309 310 311 312 313 314 315 316 317 318 319 320 321
version of op1 in the first place.

It might even be a bit disguised:

  nullFail :: C [a] => [a] -> [a]
  nullFail x = op2 x ++ op2 x

  instance C a => C [a] where
    op1 x = nullFail x

Precisely this is used in package 'regex-base', module Context.hs.
See the overlapping instances for RegexContext, and the fact that they
call 'nullFail' just like the example above.  The DoCon package also
Gabor Greif's avatar
Gabor Greif committed
322
does the same thing; it shows up in module Fraction.hs.
323

324 325 326 327 328 329
Conclusion: when typechecking the methods in a C [a] instance, we want to
treat the 'a' as an *existential* type variable, in the sense described
by Note [Binding when looking up instances].  That is why isOverlappableTyVar
responds True to an InstSkol, which is the kind of skolem we use in
tcInstDecl2.

330

331 332 333
Note [Tricky type variable scoping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In our example
dterei's avatar
dterei committed
334 335 336
        class C a where
           op1, op2 :: Ix b => a -> b -> b
           op2 = <dm-rhs>
337

dterei's avatar
dterei committed
338 339 340
        instance C a => C [a]
           {-# INLINE [2] op1 #-}
           op1 = <rhs>
341 342 343 344 345 346 347 348

note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
in scope in <rhs>.  In particular, we must make sure that 'b' is in
scope when typechecking <dm-rhs>.  This is achieved by subFunTys,
which brings appropriate tyvars into scope. This happens for both
<dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
complained if 'b' is mentioned in <rhs>.

349

350

Austin Seipp's avatar
Austin Seipp committed
351 352
************************************************************************
*                                                                      *
353
\subsection{Extracting instance decls}
Austin Seipp's avatar
Austin Seipp committed
354 355
*                                                                      *
************************************************************************
356 357

Gather up the instance declarations from their various sources
Austin Seipp's avatar
Austin Seipp committed
358
-}
359

Ian Lynagh's avatar
Ian Lynagh committed
360
tcInstDecls1    -- Deal with both source-code and imported instance decls
361
   :: [LInstDecl Name]          -- Source code instance decls
Ian Lynagh's avatar
Ian Lynagh committed
362
   -> TcM (TcGblEnv,            -- The full inst env
363
           [InstInfo Name],     -- Source-code instance decls to process;
Ian Lynagh's avatar
Ian Lynagh committed
364
                                -- contains all dfuns for this module
365
           [DerivInfo])         -- From data family instances
366

367 368
tcInstDecls1 inst_decls
  = do {    -- Do class and family instance declarations
369
       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
370

371 372 373
       ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
             fam_insts   = concat fam_insts_s
             local_infos = concat local_infos_s
374

375 376 377
       ; gbl_env <- addClsInsts local_infos $
                    addFamInsts fam_insts   $
                    getGblEnv
378

379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399
       ; return ( gbl_env
                , local_infos
                , concat datafam_deriv_infos ) }

-- | Use DerivInfo for data family instances (produced by tcInstDecls1),
--   datatype declarations (TyClDecl), and standalone deriving declarations
--   (DerivDecl) to check and process all derived class instances.
tcInstDeclsDeriv
  :: [DerivInfo]
  -> [LTyClDecl Name]
  -> [LDerivDecl Name]
  -> TcM (TcGblEnv, [InstInfo Name], HsValBinds Name)
tcInstDeclsDeriv datafam_deriv_infos tyclds derivds
  = do th_stage <- getStage -- See Note [Deriving inside TH brackets]
       if isBrackStage th_stage
       then do { gbl_env <- getGblEnv
               ; return (gbl_env, bagToList emptyBag, emptyValBindsOut) }
       else do { data_deriv_infos <- mkDerivInfos tyclds
               ; let deriv_infos = datafam_deriv_infos ++ data_deriv_infos
               ; (tcg_env, info_bag, valbinds) <- tcDeriving deriv_infos derivds
               ; return (tcg_env, bagToList info_bag, valbinds) }
400

401 402
addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
addClsInsts infos thing_inside
403
  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
404

405
addFamInsts :: [FamInst] -> TcM a -> TcM a
406 407 408
-- Extend (a) the family instance envt
--        (b) the type envt with stuff from data type decls
addFamInsts fam_insts thing_inside
409
  = tcExtendLocalFamInstEnv fam_insts $
410 411
    tcExtendGlobalEnv axioms $
    tcExtendTyConEnv data_rep_tycons  $
412
    do { traceTc "addFamInsts" (pprFamInsts fam_insts)
413 414 415
       ; tcg_env <- tcAddImplicits data_rep_tycons
                    -- Does not add its axiom; that comes from
                    -- adding the 'axioms' above
416 417
       ; setGblEnv tcg_env thing_inside }
  where
418 419 420
    axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
    data_rep_tycons = famInstsRepTyCons fam_insts
      -- The representation tycons for 'data instances' declarations
421

Austin Seipp's avatar
Austin Seipp committed
422
{-
423 424 425 426 427 428 429 430
Note [Deriving inside TH brackets]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given a declaration bracket
  [d| data T = A | B deriving( Show ) |]

there is really no point in generating the derived code for deriving(
Show) and then type-checking it. This will happen at the call site
anyway, and the type check should never fail!  Moreover (Trac #6005)
431 432
the scoping of the generated code inside the bracket does not seem to
work out.
433 434 435

The easy solution is simply not to generate the derived instances at
all.  (A less brutal solution would be to generate them with no
436
bindings.)  This will become moot when we shift to the new TH plan, so
437
the brutal solution will do.
Austin Seipp's avatar
Austin Seipp committed
438
-}
439

440
tcLocalInstDecl :: LInstDecl Name
441
                -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
Ian Lynagh's avatar
Ian Lynagh committed
442 443 444 445
        -- A source-file instance declaration
        -- Type-check all the stuff before the "where"
        --
        -- We check for respectable instance type, and context
446
tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
447
  = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
448
       ; return ([], [fam_inst], []) }
449

450
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
451 452
  = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl Nothing (L loc decl)
       ; return ([], [fam_inst], maybeToList m_deriv_info) }
453 454

tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
455 456
  = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
       ; return (insts, fam_insts, deriv_infos) }
457

458 459
tcClsInstDecl :: LClsInstDecl Name
              -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
460
-- The returned DerivInfos are for any associated data families
Simon Peyton Jones's avatar
Simon Peyton Jones committed
461 462
tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                  , cid_sigs = uprags, cid_tyfam_insts = ats
463
                                  , cid_overlap_mode = overlap_mode
Simon Peyton Jones's avatar
Simon Peyton Jones committed
464 465 466
                                  , cid_datafam_insts = adts }))
  = setSrcSpan loc                      $
    addErrCtxt (instDeclCtxt1 poly_ty)  $
467
    do  { (tyvars, theta, clas, inst_tys) <- tcHsClsInstType InstDeclCtxt poly_ty
468
        ; let mini_env   = mkVarEnv (classTyVars clas `zip` inst_tys)
469
              mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env
470
              mb_info    = Just (clas, tyvars, mini_env)
471

472
        -- Next, process any associated types.
473
        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
474 475
        ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
                           mapAndRecoverM (tcTyFamInstDecl mb_info) ats
476
        ; datafam_stuff <- tcExtendTyVarEnv tyvars $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
477
                           mapAndRecoverM (tcDataFamInstDecl mb_info) adts
478 479
        ; let (datafam_insts, m_deriv_infos) = unzip datafam_stuff
              deriv_infos                    = catMaybes m_deriv_infos
480

dreixel's avatar
dreixel committed
481
        -- Check for missing associated types and build them
482
        -- from their defaults (if available)
483
        ; let defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
484
                            `unionNameSet`
485
                            mkNameSet (map (unLoc . dfid_tycon . unLoc) adts)
486
        ; tyfam_insts1 <- mapM (tcATDefault True loc mini_subst defined_ats)
487
                               (classATItems clas)
488

Ian Lynagh's avatar
Ian Lynagh committed
489 490
        -- Finally, construct the Core representation of the instance.
        -- (This no longer includes the associated types.)
491
        ; dfun_name <- newDFunName clas inst_tys (getLoc (hsSigType poly_ty))
dterei's avatar
dterei committed
492
                -- Dfun location is that of instance *header*
493

494 495
        ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name tyvars theta
                              clas inst_tys
496

497
        ; let inst_info = InstInfo { iSpec  = ispec
498 499
                                   , iBinds = InstBindings
                                     { ib_binds = binds
500
                                     , ib_tyvars = map Var.varName tyvars -- Scope over bindings
501
                                     , ib_pragmas = uprags
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
502
                                     , ib_extensions = []
503
                                     , ib_derived = False } }
504

505 506
        ; doClsInstErrorChecks inst_info

507 508
        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts
                 , deriv_infos ) }
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
doClsInstErrorChecks :: InstInfo Name -> TcM ()
doClsInstErrorChecks inst_info
 = do { traceTc "doClsInstErrorChecks" (ppr ispec)
      ; dflags <- getDynFlags
      ; is_boot <- tcIsHsBootOrSig

         -- In hs-boot files there should be no bindings
      ; failIfTc (is_boot && not no_binds) badBootDeclErr

         -- Handwritten instances of the poly-kinded Typeable
         -- class are always forbidden
      ; failIfTc (clas_nm == typeableClassName) typeable_err

         -- Check for hand-written Generic instances (disallowed in Safe Haskell)
      ; when (clas_nm `elem` genericClassNames) $
        do { failIfTc (safeLanguageOn dflags) gen_inst_err
           ; when (safeInferOn dflags) (recordUnsafeInfer emptyBag) }
  }
  where
    ispec    = iSpec inst_info
    binds    = iBinds inst_info
    no_binds = isEmptyLHsBinds (ib_binds binds) && null (ib_pragmas binds)
    clas_nm  = is_cls_nm ispec

    gen_inst_err = hang (text ("Generic instances can only be "
                            ++ "derived in Safe Haskell.") $+$
                         text "Replace the following instance:")
                      2 (pprInstanceHdr ispec)

    -- Report an error or a warning for a Typeable instances.
    -- If we are working on an .hs-boot file, we just report a warning,
    -- and ignore the instance.  We do this, to give users a chance to fix
    -- their code.
    typeable_err = text "Class" <+> quotes (ppr clas_nm)
                    <+> text "does not support user-specified instances"

Austin Seipp's avatar
Austin Seipp committed
547 548 549
{-
************************************************************************
*                                                                      *
550
               Type checking family instances
Austin Seipp's avatar
Austin Seipp committed
551 552
*                                                                      *
************************************************************************
553 554 555 556 557

Family instances are somewhat of a hybrid.  They are processed together with
class instance heads, but can contain data constructors and hence they share a
lot of kinding and type checking code with ordinary algebraic data types (and
GADTs).
Austin Seipp's avatar
Austin Seipp committed
558
-}
559

560
tcFamInstDeclCombined :: Maybe ClsInstInfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
561 562
                      -> Located Name -> TcM TyCon
tcFamInstDeclCombined mb_clsinfo fam_tc_lname
563
  = do { -- Type family instances require -XTypeFamilies
564
         -- and can't (currently) be in an hs-boot file
565
       ; traceTc "tcFamInstDecl" (ppr fam_tc_lname)
566
       ; type_families <- xoptM LangExt.TypeFamilies
567
       ; is_boot <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
568 569 570 571 572 573
       ; checkTc type_families $ badFamInstDecl fam_tc_lname
       ; checkTc (not is_boot) $ badBootFamInstDeclErr

       -- Look up the family TyCon and check for validity including
       -- check that toplevel type instances are not for associated types.
       ; fam_tc <- tcLookupLocatedTyCon fam_tc_lname
Simon Peyton Jones's avatar
Simon Peyton Jones committed
574 575
       ; when (isNothing mb_clsinfo &&   -- Not in a class decl
               isTyConAssoc fam_tc)      -- but an associated type
576 577
              (addErr $ assocInClassErr fam_tc_lname)

578
       ; return fam_tc }
579

580
tcTyFamInstDecl :: Maybe ClsInstInfo
581
                -> LTyFamInstDecl Name -> TcM FamInst
582
  -- "type instance"
583
tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
584 585
  = setSrcSpan loc           $
    tcAddTyFamInstCtxt decl  $
586
    do { let fam_lname = tfe_tycon (unLoc eqn)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
587 588 589
       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname

         -- (0) Check it's an open type family
Jan Stolarek's avatar
Jan Stolarek committed
590 591
       ; checkTc (isFamilyTyCon fam_tc)         (notFamily fam_tc)
       ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
592
       ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
593

594
         -- (1) do the work of verifying the synonym group
595
       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) mb_clsinfo eqn
596

597
         -- (2) check for validity
Jan Stolarek's avatar
Jan Stolarek committed
598
       ; checkValidCoAxBranch mb_clsinfo fam_tc co_ax_branch
599

600
         -- (3) construct coercion axiom
601
       ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
602 603
       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
       ; newFamInst SynFamilyInst axiom }
604

605
tcDataFamInstDecl :: Maybe ClsInstInfo
606
                  -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo)
607
  -- "newtype instance" and "data instance"
608
tcDataFamInstDecl mb_clsinfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
609 610 611 612
    (L loc decl@(DataFamInstDecl
       { dfid_pats = pats
       , dfid_tycon = fam_tc_name
       , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
613 614
                                     , dd_ctxt = ctxt, dd_cons = cons
                                     , dd_derivs = derivs } }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
615 616 617 618 619 620
  = setSrcSpan loc             $
    tcAddDataFamInstCtxt decl  $
    do { fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_tc_name

         -- Check that the family declaration is for the right kind
       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
621
       ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
622

dreixel's avatar
dreixel committed
623
         -- Kind check type patterns
624
       ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
625
                     (kcDataDefn (unLoc fam_tc_name) pats defn) $
626
           \tvs' pats' res_kind -> do
627
       {
628 629 630
         -- Check that left-hand sides are ok (mono-types, no type families,
         -- consistent instantiations, etc)
       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
631

dreixel's avatar
dreixel committed
632
         -- Result kind must be '*' (otherwise, we have too few patterns)
633
       ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
634

635 636
       ; stupid_theta <- solveEqualities $ tcHsContext ctxt
       ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv stupid_theta
637
       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
638

dreixel's avatar
dreixel committed
639
         -- Construct representation tycon
640
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
641
       ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
642 643 644 645 646 647 648 649
       ; let (eta_pats, etad_tvs) = eta_reduce pats'
             eta_tvs              = filterOut (`elem` etad_tvs) tvs'
             full_tvs             = eta_tvs ++ etad_tvs
                 -- Put the eta-removed tyvars at the end
                 -- Remember, tvs' is in arbitrary order (except kind vars are
                 -- first, so there is no reason to suppose that the etad_tvs
                 -- (obtained from the pats) are at the end (Trac #11148)
             orig_res_ty          = mkTyConApp fam_tc pats'
650

651
       ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
652
           do { let ty_binders = mkTyConBindersPreferAnon full_tvs liftedTypeKind
653
              ; data_cons <- tcConDecls new_or_data
654
                                        rec_rep_tc
655
                                        (ty_binders, orig_res_ty) cons
656 657 658 659
              ; tc_rhs <- case new_or_data of
                     DataType -> return (mkDataTyConRhs data_cons)
                     NewType  -> ASSERT( not (null data_cons) )
                                 mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
660
              -- freshen tyvars
661
              ; let axiom  = mkSingleCoAxiom Representational
662
                                             axiom_name eta_tvs [] fam_tc eta_pats
663 664
                                             (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                    parent = DataFamInstTyCon axiom fam_tc pats'
665

666 667

                      -- NB: Use the full_tvs from the pats. See bullet toward
668
                      -- the end of Note [Data type families] in TyCon
669
                    rep_tc   = mkAlgTyCon rep_tc_name
670
                                          ty_binders liftedTypeKind
671 672 673 674
                                          (map (const Nominal) full_tvs)
                                          (fmap unLoc cType) stupid_theta
                                          tc_rhs parent
                                          Recursive gadt_syntax
675 676 677 678 679
                 -- We always assume that indexed types are recursive.  Why?
                 -- (1) Due to their open nature, we can never be sure that a
                 -- further instance might not introduce a new recursive
                 -- dependency.  (2) They are always valid loop breakers as
                 -- they involve a coercion.
680
              ; return (rep_tc, axiom) }
681 682

         -- Remember to check validity; no recursion to worry about here
683
       ; checkValidTyCon rep_tc
684 685 686 687 688 689 690 691

       ; let m_deriv_info = case derivs of
               Nothing          -> Nothing
               Just (L _ preds) ->
                 Just $ DerivInfo { di_rep_tc = rep_tc
                                  , di_preds  = preds
                                  , di_ctxt   = tcMkDataFamInstCtxt decl }

692
       ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
693
       ; return (fam_inst, m_deriv_info) } }
694
  where
695 696 697 698 699 700 701 702 703 704 705
    eta_reduce :: [Type] -> ([Type], [TyVar])
    -- See Note [Eta reduction for data families] in FamInstEnv
    -- Splits the incoming patterns into two: the [TyVar]
    -- are the patterns that can be eta-reduced away.
    -- e.g.     T [a] Int a d c   ==>  (T [a] Int a, [d,c])
    --
    -- NB: quadratic algorithm, but types are small here
    eta_reduce pats
      = go (reverse pats) []
    go (pat:pats) etad_tvs
      | Just tv <- getTyVar_maybe pat
706
      , not (tv `elemVarSet` tyCoVarsOfTypes pats)
707 708
      = go pats (tv : etad_tvs)
    go pats etad_tvs = (reverse pats, etad_tvs)
709

710

711
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
712
*                                                                      *
713
      Type-checking instance declarations, pass 2
Austin Seipp's avatar
Austin Seipp committed
714
*                                                                      *
715
********************************************************************* -}
716

717
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
718
             -> TcM (LHsBinds Id)
Ian Lynagh's avatar
Ian Lynagh committed
719 720
-- (a) From each class declaration,
--      generate any default-method bindings
721
-- (b) From each instance decl
Ian Lynagh's avatar
Ian Lynagh committed
722
--      generate the dfun binding
723 724

tcInstDecls2 tycl_decls inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
725
  = do  { -- (a) Default methods from class decls
726
          let class_decls = filter (isClassDecl . unLoc) tycl_decls
727
        ; dm_binds_s <- mapM tcClassDecl2 class_decls
728
        ; let dm_binds = unionManyBags dm_binds_s
dterei's avatar
dterei committed
729

Ian Lynagh's avatar
Ian Lynagh committed
730
          -- (b) instance declarations
dterei's avatar
dterei committed
731 732
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
733
              -- (they were arready added in TcTyDecls.tcAddImplicits)
734
              -- See Note [Default methods in the type environment]
735
        ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
736
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
737 738

          -- Done
739
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
740

741 742
{- Note [Default methods in the type environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743
The default method Ids are already in the type environment (see Note
744
[Default method Ids and Template Haskell] in TcTyDcls), BUT they
745 746 747 748 749 750
don't have their InlinePragmas yet.  Usually that would not matter,
because the simplifier propagates information from binding site to
use.  But, unusually, when compiling instance decls we *copy* the
INLINE pragma from the default method to the method for that
particular operation (see Note [INLINE and default methods] below).

751
So right here in tcInstDecls2 we must re-extend the type envt with
752
the default method Ids replete with their INLINE pragmas.  Urk.
Austin Seipp's avatar
Austin Seipp committed
753
-}
754

755 756 757 758 759
tcInstDecl2 :: InstInfo Name -> TcM (LHsBinds Id)
            -- Returns a binding for the dfun
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
  = recoverM (return emptyLHsBinds)             $
    setSrcSpan loc                              $
dterei's avatar
dterei committed
760
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
761
    do {  -- Instantiate the instance decl with skolem constants
762
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
763
       ; dfun_ev_vars <- newEvVars dfun_theta
dimitris's avatar
dimitris committed
764 765 766
                     -- We instantiate the dfun_id with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
767

768
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
769
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
niteria's avatar
niteria committed
770
             sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
771

772
       ; traceTc "tcInstDecl2" (vcat [ppr inst_tyvars, ppr inst_tys, ppr dfun_theta, ppr sc_theta'])
773

774 775
                      -- Deal with 'SPECIALISE instance' pragmas
                      -- See Note [SPECIALISE instance pragmas]
776
       ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
777

778 779 780 781 782 783
         -- Typecheck superclasses and methods
         -- See Note [Typechecking plan for instance declarations]
       ; dfun_ev_binds_var <- newTcEvBinds
       ; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
       ; ((sc_meth_ids, sc_meth_binds, sc_meth_implics), tclvl)
             <- pushTcLevelM $
784
                do { (sc_ids, sc_binds, sc_implics)
785
                        <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
786
                                          inst_tys dfun_ev_binds
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803
                                          sc_theta'

                      -- Typecheck the methods
                   ; (meth_ids, meth_binds, meth_implics)
                        <- tcMethods dfun_id clas inst_tyvars dfun_ev_vars
                                     inst_tys dfun_ev_binds spec_inst_info
                                     op_items ibinds

                   ; return ( sc_ids     ++          meth_ids
                            , sc_binds   `unionBags` meth_binds
                            , sc_implics `unionBags` meth_implics ) }

       ; env <- getLclEnv
       ; emitImplication $ Implic { ic_tclvl  = tclvl
                                  , ic_skols  = inst_tyvars
                                  , ic_no_eqs = False
                                  , ic_given  = dfun_ev_vars
804
                                  , ic_wanted = mkImplicWC sc_meth_implics
805
                                  , ic_status = IC_Unsolved
806
                                  , ic_binds  = Just dfun_ev_binds_var
807 808
                                  , ic_env    = env
                                  , ic_info   = InstSkol }
809

810
       -- Create the result bindings
batterseapower's avatar
batterseapower committed
811
       ; self_dict <- newDict clas inst_tys
812 813
       ; let class_tc      = classTyCon clas
             [dict_constr] = tyConDataCons class_tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
814 815
             dict_bind     = mkVarBind self_dict (L loc con_app_args)

816 817 818 819
                     -- We don't produce a binding for the dict_constr; instead we
                     -- rely on the simplifier to unfold this saturated application
                     -- We do this rather than generate an HsCon directly, because
                     -- it means that the special cases (e.g. dictionary with only one
dterei's avatar
dterei committed
820
                     -- member) are dealt with by the common MkId.mkDataConWrapId
dterei's avatar
dterei committed
821 822