TcInstDcls.hs 74.8 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, 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 TcPat      ( addInlinePrags, lookupPragEnv, emptyPragEnv )
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
dterei's avatar
dterei committed
36
import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
37
import Type
38
import TcEvidence
39
import TyCon
40 41
import Coercion   ( emptyCvSubstEnv )
import CoAxiom
42 43 44
import DataCon
import Class
import Var
45
import VarEnv
46
import VarSet
47
import PrelNames  ( typeableClassName, genericClassNames )
dterei's avatar
dterei committed
48 49 50
import Bag
import BasicTypes
import DynFlags
51
import ErrUtils
dterei's avatar
dterei committed
52
import FastString
53
import HscTypes ( isHsBootOrSig )
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
import Data.List  ( partition )
67

68 69


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

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.

81 82 83

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

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

dterei's avatar
dterei committed
91 92 93
        instance C a => C [a]
           {-# INLINE [2] op1 #-}
           op1 = <rhs>
94
===>
dterei's avatar
dterei committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
        -- 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
113
        op1_i = /\a. \(d:C a).
dterei's avatar
dterei committed
114 115 116 117 118 119 120 121 122 123 124 125
               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
126
        op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
dterei's avatar
dterei committed
127 128 129 130 131 132 133

        -- 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
134

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

139 140
Note [Instances and loop breakers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
141
* Note that df_i may be mutually recursive with both op1_i and op2_i.
dterei's avatar
dterei committed
142
  It's crucial that df_i is not chosen as the loop breaker, even
143 144 145 146 147 148
  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
149
  the first place.)
150 151 152

* 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
153
  loop-breaker because df_i isn't), op1_i will ironically never be
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
154 155 156 157
  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

158 159 160 161 162 163 164 165 166 167
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
168
But it's tricky to make this work in practice, because it requires us to
169
inline both 'op2' and 'df'.  But neither is keen to inline without having
dterei's avatar
dterei committed
170
seen the other's result; and it's very easy to get code bloat (from the
171 172 173
big intermediate) if you inline a bit too much.

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

 * 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
183
   a suitable constructor application -- inlining df "on the fly" as it
184 185
   were.

186 187 188
 * 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
189

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

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

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

202 203 204
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.
205 206 207 208 209 210

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

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

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

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

218
Instead, we simply rely on the fact that casts are cheap:
219

220
   $df :: forall a. C a => C [a]
221
   {-# INLINE df #-}  -- NB: INLINE this
222 223
   $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
224

225 226
   $cop_list :: forall a. C a => [a] -> [a]
   $cop_list = <blah>
227

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

233 234 235 236 237
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
238
wasn't due to the indirection).
239

dterei's avatar
dterei committed
240
There is an awkward wrinkle though: we want to be very
241
careful when we have
242 243 244
    instance C a => C [a] where
      {-# INLINE op #-}
      op = ...
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
245 246
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
247
dictionary and the list argument).  So we must not eta-expand $df
dterei's avatar
dterei committed
248
above.  We ensure that this doesn't happen by putting an INLINE
249 250
pragma on the dfun itself; after all, it ends up being just a cast.

dterei's avatar
dterei committed
251
There is one more dark corner to the INLINE story, even more deeply
252 253 254 255 256 257 258
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
259

260 261
    class DeepSeq a where
      deepSeq :: a -> b -> b
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
    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
290

291 292 293 294 295 296 297
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 = ...
298
  instance C [Int] where
299 300 301 302 303 304 305
    ...

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
306
instance.
307

dterei's avatar
dterei committed
308
Why is this justified?  Because we generate a (C [a]) constraint in
309
a context in which 'a' cannot be instantiated to anything that matches
Gabor Greif's avatar
Gabor Greif committed
310
other overlapping instances, or else we would not be executing this
311 312 313 314 315 316 317 318 319 320 321 322 323
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
324
does the same thing; it shows up in module Fraction.hs.
325

326 327 328 329 330 331
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.

332

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

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

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>.

351

352

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

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

Ian Lynagh's avatar
Ian Lynagh committed
362
tcInstDecls1    -- Deal with both source-code and imported instance decls
363
   :: [TyClGroup Name]          -- For deriving stuff
Ian Lynagh's avatar
Ian Lynagh committed
364 365 366
   -> [LInstDecl Name]          -- Source code instance decls
   -> [LDerivDecl Name]         -- Source code stand-alone deriving decls
   -> TcM (TcGblEnv,            -- The full inst env
367
           [InstInfo Name],     -- Source-code instance decls to process;
Ian Lynagh's avatar
Ian Lynagh committed
368 369
                                -- contains all dfuns for this module
           HsValBinds Name)     -- Supporting bindings for derived instances
370

371
tcInstDecls1 tycl_decls inst_decls deriv_decls
372
  = checkNoErrs $
373 374 375 376
    do {    -- Stop if addInstInfos etc discovers any errors
            -- (they recover, so that we get more than one error each
            -- round)

377
            -- Do class and family instance declarations
378
       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
379
       ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
380 381 382 383
             fam_insts    = concat fam_insts_s
             local_infos' = concat local_infos_s
             -- Handwritten instances of the poly-kinded Typeable class are
             -- forbidden, so we handle those separately
384
             (typeable_instances, local_infos)
385
                = partition bad_typeable_instance local_infos'
386

387 388
       ; addClsInsts local_infos $
         addFamInsts fam_insts   $
389
    do {    -- Compute instances from "deriving" clauses;
390 391 392 393
            -- This stuff computes a context for the derived instance
            -- decl, so it needs to know about all the instances possible
            -- NB: class instance declarations can contain derivings as
            --     part of associated data type declarations
394
         failIfErrsM    -- If the addInsts stuff gave any errors, don't
dterei's avatar
dterei committed
395 396
                        -- try the deriving stuff, because that may give
                        -- more errors still
dreixel's avatar
dreixel committed
397

398
       ; traceTc "tcDeriving" Outputable.empty
399
       ; th_stage <- getStage   -- See Note [Deriving inside TH brackets ]
400
       ; (gbl_env, deriv_inst_info, deriv_binds)
401
              <- if isBrackStage th_stage
402 403
                 then do { gbl_env <- getGblEnv
                         ; return (gbl_env, emptyBag, emptyValBindsOut) }
404 405 406 407
                 else do { data_deriv_infos <- mkDerivInfos tycl_decls
                         ; let deriv_infos = concat datafam_deriv_infos ++
                                             data_deriv_infos
                         ; tcDeriving deriv_infos deriv_decls }
408

409
       -- Fail if there are any handwritten instance of poly-kinded Typeable
410
       ; mapM_ typeable_err typeable_instances
411

412
       -- Check that if the module is compiled with -XSafe, there are no
413
       -- hand written instances of old Typeable as then unsafe casts could be
dreixel's avatar
dreixel committed
414
       -- performed. Derived instances are OK.
415
       ; dflags <- getDynFlags
416 417 418 419
       ; when (safeLanguageOn dflags) $ forM_ local_infos $ \x -> case x of
             _ | genInstCheck x -> addErrAt (getSrcSpan $ iSpec x) (genInstErr x)
             _ -> return ()

420
       -- As above but for Safe Inference mode.
421
       ; when (safeInferOn dflags) $ forM_ local_infos $ \x -> case x of
422
             _ | genInstCheck x -> recordUnsafeInfer emptyBag
423
             _ -> return ()
424

dreixel's avatar
dreixel committed
425
       ; return ( gbl_env
426
                , bagToList deriv_inst_info ++ local_infos
427
                , deriv_binds )
428
    }}
dterei's avatar
dterei committed
429
  where
430
    -- Separate the Typeable instances from the rest
431 432 433
    bad_typeable_instance i
      = typeableClassName == is_cls_nm (iSpec i)

434
    -- Check for hand-written Generic instances (disallowed in Safe Haskell)
435
    genInstCheck ty = is_cls_nm (iSpec ty) `elem` genericClassNames
436
    genInstErr i = hang (text ("Generic instances can only be "
437
                            ++ "derived in Safe Haskell.") $+$
438
                         text "Replace the following instance:")
439
                     2 (pprInstanceHdr (iSpec i))
440

441
    -- Report an error or a warning for a Typeable instances.
442
    -- If we are working on an .hs-boot file, we just report a warning,
443 444 445 446 447
    -- and ignore the instance.  We do this, to give users a chance to fix
    -- their code.
    typeable_err i =
      setSrcSpan (getSrcSpan (iSpec i)) $
        do env <- getGblEnv
448
           if isHsBootOrSig (tcg_src env)
449 450 451
             then
               do warn <- woptM Opt_WarnDerivingTypeable
                  when warn $ addWarnTc $ vcat
452 453
                    [ ppTypeable <+> text "instances in .hs-boot files are ignored"
                    , text "This warning will become an error in future versions of the compiler"
454
                    ]
455 456
             else addErrTc $ text "Class" <+> ppTypeable
                             <+> text "does not support user-specified instances"
457 458
    ppTypeable :: SDoc
    ppTypeable = quotes (ppr typeableClassName)
459

460 461
addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
addClsInsts infos thing_inside
462
  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
463

464
addFamInsts :: [FamInst] -> TcM a -> TcM a
465 466 467
-- Extend (a) the family instance envt
--        (b) the type envt with stuff from data type decls
addFamInsts fam_insts thing_inside
468
  = tcExtendLocalFamInstEnv fam_insts $
469 470
    tcExtendGlobalEnv axioms $
    tcExtendTyConEnv data_rep_tycons  $
471
    do { traceTc "addFamInsts" (pprFamInsts fam_insts)
472 473 474
       ; tcg_env <- tcAddImplicits data_rep_tycons
                    -- Does not add its axiom; that comes from
                    -- adding the 'axioms' above
475 476
       ; setGblEnv tcg_env thing_inside }
  where
477 478 479
    axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
    data_rep_tycons = famInstsRepTyCons fam_insts
      -- The representation tycons for 'data instances' declarations
480

Austin Seipp's avatar
Austin Seipp committed
481
{-
482 483 484 485 486 487 488 489
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)
490 491
the scoping of the generated code inside the bracket does not seem to
work out.
492 493 494

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

499
tcLocalInstDecl :: LInstDecl Name
500
                -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
Ian Lynagh's avatar
Ian Lynagh committed
501 502 503 504
        -- A source-file instance declaration
        -- Type-check all the stuff before the "where"
        --
        -- We check for respectable instance type, and context
505
tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
506
  = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
507
       ; return ([], [fam_inst], []) }
508

509
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
510 511
  = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl Nothing (L loc decl)
       ; return ([], [fam_inst], maybeToList m_deriv_info) }
512 513

tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
514 515
  = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
       ; return (insts, fam_insts, deriv_infos) }
516

517 518 519
tcClsInstDecl :: LClsInstDecl Name
              -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
-- the returned DerivInfos are for any associated data families
Simon Peyton Jones's avatar
Simon Peyton Jones committed
520 521
tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                  , cid_sigs = uprags, cid_tyfam_insts = ats
522
                                  , cid_overlap_mode = overlap_mode
Simon Peyton Jones's avatar
Simon Peyton Jones committed
523 524 525
                                  , cid_datafam_insts = adts }))
  = setSrcSpan loc                      $
    addErrCtxt (instDeclCtxt1 poly_ty)  $
526
    do  { is_boot <- tcIsHsBootOrSig
Ian Lynagh's avatar
Ian Lynagh committed
527 528 529
        ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
                  badBootDeclErr

530
        ; (tyvars, theta, clas, inst_tys) <- tcHsClsInstType InstDeclCtxt poly_ty
531
        ; let mini_env   = mkVarEnv (classTyVars clas `zip` inst_tys)
532 533
              mini_subst = mkTCvSubst (mkInScopeSet (mkVarSet tyvars))
                                      (mini_env, emptyCvSubstEnv)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
534
              mb_info    = Just (clas, mini_env)
535

536
        -- Next, process any associated types.
537
        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
538 539
        ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
                           mapAndRecoverM (tcTyFamInstDecl mb_info) ats
540
        ; datafam_stuff <- tcExtendTyVarEnv tyvars $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
541
                           mapAndRecoverM (tcDataFamInstDecl mb_info) adts
542 543
        ; let (datafam_insts, m_deriv_infos) = unzip datafam_stuff
              deriv_infos                    = catMaybes m_deriv_infos
544

dreixel's avatar
dreixel committed
545
        -- Check for missing associated types and build them
546
        -- from their defaults (if available)
547
        ; let defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
548
                            `unionNameSet`
549
                            mkNameSet (map (unLoc . dfid_tycon . unLoc) adts)
550
        ; tyfam_insts1 <- mapM (tcATDefault True loc mini_subst defined_ats)
551
                               (classATItems clas)
552

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

558 559
        ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name tyvars theta
                              clas inst_tys
560
        ; let inst_info = InstInfo { iSpec  = ispec
561 562
                                   , iBinds = InstBindings
                                     { ib_binds = binds
563
                                     , ib_tyvars = map Var.varName tyvars -- Scope over bindings
564
                                     , ib_pragmas = uprags
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
565
                                     , ib_extensions = []
566
                                     , ib_derived = False } }
567

568 569
        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts
                 , deriv_infos ) }
570

571

Austin Seipp's avatar
Austin Seipp committed
572 573 574
{-
************************************************************************
*                                                                      *
575
               Type checking family instances
Austin Seipp's avatar
Austin Seipp committed
576 577
*                                                                      *
************************************************************************
578 579 580 581 582

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
583
-}
584

585
tcFamInstDeclCombined :: Maybe ClsInfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
586 587
                      -> Located Name -> TcM TyCon
tcFamInstDeclCombined mb_clsinfo fam_tc_lname
588
  = do { -- Type family instances require -XTypeFamilies
589
         -- and can't (currently) be in an hs-boot file
590
       ; traceTc "tcFamInstDecl" (ppr fam_tc_lname)
591
       ; type_families <- xoptM LangExt.TypeFamilies
592
       ; is_boot <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
593 594 595 596 597 598
       ; 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
599 600
       ; when (isNothing mb_clsinfo &&   -- Not in a class decl
               isTyConAssoc fam_tc)      -- but an associated type
601 602
              (addErr $ assocInClassErr fam_tc_lname)

603
       ; return fam_tc }
604

605
tcTyFamInstDecl :: Maybe ClsInfo
606
                -> LTyFamInstDecl Name -> TcM FamInst
607
  -- "type instance"
608
tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
609 610
  = setSrcSpan loc           $
    tcAddTyFamInstCtxt decl  $
611
    do { let fam_lname = tfe_tycon (unLoc eqn)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
612 613 614
       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname

         -- (0) Check it's an open type family
Jan Stolarek's avatar
Jan Stolarek committed
615 616
       ; checkTc (isFamilyTyCon fam_tc)         (notFamily fam_tc)
       ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
617
       ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
618

619
         -- (1) do the work of verifying the synonym group
620
       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) mb_clsinfo eqn
621

622
         -- (2) check for validity
Jan Stolarek's avatar
Jan Stolarek committed
623
       ; checkValidCoAxBranch mb_clsinfo fam_tc co_ax_branch
624

625
         -- (3) construct coercion axiom
626
       ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
627 628
       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
       ; newFamInst SynFamilyInst axiom }
629

630 631
tcDataFamInstDecl :: Maybe ClsInfo
                  -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo)
632
  -- "newtype instance" and "data instance"
633
tcDataFamInstDecl mb_clsinfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
634 635 636 637
    (L loc decl@(DataFamInstDecl
       { dfid_pats = pats
       , dfid_tycon = fam_tc_name
       , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
638 639
                                     , dd_ctxt = ctxt, dd_cons = cons
                                     , dd_derivs = derivs } }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
640 641 642 643 644 645
  = 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)
646
       ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
647

dreixel's avatar
dreixel committed
648
         -- Kind check type patterns
649
       ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
650
                     (kcDataDefn (unLoc fam_tc_name) pats defn) $
651
           \tvs' pats' res_kind -> do
652
       {
653 654 655
         -- Check that left-hand sides are ok (mono-types, no type families,
         -- consistent instantiations, etc)
       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
656

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

660 661
       ; stupid_theta <- solveEqualities $ tcHsContext ctxt
       ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv stupid_theta
662
       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
663

dreixel's avatar
dreixel committed
664
         -- Construct representation tycon
665
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
666
       ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
667 668 669 670 671 672 673 674
       ; 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'
675 676

       ; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
677 678
           do { data_cons <- tcConDecls new_or_data
                                        rec_rep_tc
679
                                        (full_tvs, orig_res_ty) cons
680 681 682 683
              ; 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)
684
              -- freshen tyvars
685
              ; let axiom  = mkSingleCoAxiom Representational
686
                                             axiom_name eta_tvs [] fam_tc eta_pats
687 688
                                             (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                    parent = DataFamInstTyCon axiom fam_tc pats'
689 690
                    kind   = mkPiTypesPreferFunTy tvs' liftedTypeKind

691 692

                      -- NB: Use the full_tvs from the pats. See bullet toward
693
                      -- the end of Note [Data type families] in TyCon
694 695 696 697 698
                    rep_tc   = mkAlgTyCon rep_tc_name kind full_tvs
                                             (map (const Nominal) full_tvs)
                                             (fmap unLoc cType) stupid_theta
                                             tc_rhs parent
                                             Recursive gadt_syntax
699 700 701 702 703
                 -- 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.
704
              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
705 706 707
              ; return (rep_tc, fam_inst) }

         -- Remember to check validity; no recursion to worry about here
708
       ; checkValidTyCon rep_tc
709 710 711 712 713 714 715 716 717

       ; 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 }

       ; return (fam_inst, m_deriv_info) } }
718
  where
719 720 721 722 723 724 725 726 727 728 729
    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
730
      , not (tv `elemVarSet` tyCoVarsOfTypes pats)
731 732
      = go pats (tv : etad_tvs)
    go pats etad_tvs = (reverse pats, etad_tvs)
733

734

735
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
736
*                                                                      *
737
      Type-checking instance declarations, pass 2
Austin Seipp's avatar
Austin Seipp committed
738
*                                                                      *
739
********************************************************************* -}
740

741
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
742
             -> TcM (LHsBinds Id)
Ian Lynagh's avatar
Ian Lynagh committed
743 744
-- (a) From each class declaration,
--      generate any default-method bindings
745
-- (b) From each instance decl
Ian Lynagh's avatar
Ian Lynagh committed
746
--      generate the dfun binding
747 748

tcInstDecls2 tycl_decls inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
749
  = do  { -- (a) Default methods from class decls
750
          let class_decls = filter (isClassDecl . unLoc) tycl_decls
751
        ; dm_binds_s <- mapM tcClassDecl2 class_decls
752
        ; let dm_binds = unionManyBags dm_binds_s
dterei's avatar
dterei committed
753

Ian Lynagh's avatar
Ian Lynagh committed
754
          -- (b) instance declarations
dterei's avatar
dterei committed
755 756 757
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
              -- See Note [Default methods and instances]
758
        ; inst_binds_s <- tcExtendLetEnv TopLevel dm_ids $
759
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
760 761

          -- Done
762
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
763

Austin Seipp's avatar
Austin Seipp committed
764
{-
765 766 767 768 769 770 771 772 773 774
See Note [Default methods and instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The default method Ids are already in the type environment (see Note
[Default method Ids and Template Haskell] in TcTyClsDcls), BUT they
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).

775
So right here in tcInstDecls2 we must re-extend the type envt with
776
the default method Ids replete with their INLINE pragmas.  Urk.
Austin Seipp's avatar
Austin Seipp committed
777
-}
778

779 780 781 782 783
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
784
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
785
    do {  -- Instantiate the instance decl with skolem constants
786
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id)
787
       ; dfun_ev_vars <- newEvVars dfun_theta
dimitris's avatar
dimitris committed
788 789 790
                     -- We instantiate the dfun_id with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
791

792
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
793
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
niteria's avatar
niteria committed
794
             sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
795

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

798 799
                      -- Deal with 'SPECIALISE instance' pragmas
                      -- See Note [SPECIALISE instance pragmas]
800
       ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
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
         -- 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 $
                do { fam_envs <- tcGetFamInstEnvs
                   ; (sc_ids, sc_binds, sc_implics)
                        <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
                                          inst_tys dfun_ev_binds fam_envs
                                          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
829
                                  , ic_wanted = mkImplicWC sc_meth_implics
830
                                  , ic_status = IC_Unsolved
831
                                  , ic_binds  = Just dfun_ev_binds_var
832 833
                                  , ic_env    = env
                                  , ic_info   = InstSkol }
834
<