TcInstDcls.hs 77.1 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 #-}
10 11
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
Ian Lynagh's avatar
Ian Lynagh committed
12

13
module TcInstDcls ( tcInstDecls1, tcInstDeclsDeriv, tcInstDecls2 ) where
14

dterei's avatar
dterei committed
15 16
#include "HsVersions.h"

17 18
import GhcPrelude

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

71
import Control.Monad
72
import Maybes
73 74


Austin Seipp's avatar
Austin Seipp committed
75
{-
76
Typechecking instance declarations is done in two passes. The first
77 78
pass, made by @tcInstDecls1@, collects information to be used in the
second pass.
79 80 81 82 83 84 85

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.

86 87 88

Note [How instance declarations are translated]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jan Stolarek's avatar
Jan Stolarek committed
89
Here is how we translate instance declarations into Core
90 91

Running example:
dterei's avatar
dterei committed
92 93 94
        class C a where
           op1, op2 :: Ix b => a -> b -> b
           op2 = <dm-rhs>
95

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

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

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

144 145
Note [Instances and loop breakers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
146
* Note that df_i may be mutually recursive with both op1_i and op2_i.
dterei's avatar
dterei committed
147
  It's crucial that df_i is not chosen as the loop breaker, even
148 149 150 151
  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
152
  df_i, leaving a *self*-recursive op1_i.  (If op1_i doesn't call op at
153
  the same type, it won't mention df_i, so there won't be recursion in
dterei's avatar
dterei committed
154
  the first place.)
155 156 157

* 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
158
  loop-breaker because df_i isn't), op1_i will ironically never be
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
159 160 161 162
  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

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

Instead we use a cunning trick.
dterei's avatar
dterei committed
179
 * We arrange that 'df' and 'op2' NEVER inline.
180 181 182 183 184 185 186 187

 * 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
188
   a suitable constructor application -- inlining df "on the fly" as it
189 190
   were.

191 192 193
 * 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
194

Gabor Greif's avatar
Gabor Greif committed
195
 * We make 'df' CONLIKE, so that shared uses still match; eg
196 197 198 199 200
      let d = df d1 d2
      in ...(op2 d)...(op1 d)...

Note [Single-method classes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
201
If the class has just one method (or, more accurately, just one element
202
of {superclasses + methods}), then we use a different strategy.
203 204 205 206

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

207 208 209
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.
210 211 212 213 214 215

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

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

216 217 218
   MkC :: forall a. (a->a) -> C a
   MkC = /\a.\op. op |> (sym Co:C a)

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

223
Instead, we simply rely on the fact that casts are cheap:
224

225
   $df :: forall a. C a => C [a]
226
   {-# INLINE df #-}  -- NB: INLINE this
227 228
   $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
229

230 231
   $cop_list :: forall a. C a => [a] -> [a]
   $cop_list = <blah>
232

233 234 235 236
So if we see
   (op ($df a d))
we'll inline 'op' and '$df', since both are simply casts, and
good things happen.
237

238 239 240 241 242
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
243
wasn't due to the indirection).
244

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

dterei's avatar
dterei committed
256
There is one more dark corner to the INLINE story, even more deeply
257 258 259 260 261 262 263
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
264

265 266
    class DeepSeq a where
      deepSeq :: a -> b -> b
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
    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
295

296 297 298 299 300 301 302
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 = ...
303
  instance C [Int] where
304 305 306 307 308 309 310
    ...

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
311
instance.
312

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

331 332 333 334 335 336
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.

337

338 339 340
Note [Tricky type variable scoping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In our example
dterei's avatar
dterei committed
341 342 343
        class C a where
           op1, op2 :: Ix b => a -> b -> b
           op2 = <dm-rhs>
344

dterei's avatar
dterei committed
345 346 347
        instance C a => C [a]
           {-# INLINE [2] op1 #-}
           op1 = <rhs>
348 349 350 351 352 353 354 355

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

356

357

Austin Seipp's avatar
Austin Seipp committed
358 359
************************************************************************
*                                                                      *
360
\subsection{Extracting instance decls}
Austin Seipp's avatar
Austin Seipp committed
361 362
*                                                                      *
************************************************************************
363 364

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

Ian Lynagh's avatar
Ian Lynagh committed
367
tcInstDecls1    -- Deal with both source-code and imported instance decls
368
   :: [LInstDecl GhcRn]         -- Source code instance decls
Ian Lynagh's avatar
Ian Lynagh committed
369
   -> TcM (TcGblEnv,            -- The full inst env
370
           [InstInfo GhcRn],    -- Source-code instance decls to process;
Ian Lynagh's avatar
Ian Lynagh committed
371
                                -- contains all dfuns for this module
372
           [DerivInfo])         -- From data family instances
373

374 375
tcInstDecls1 inst_decls
  = do {    -- Do class and family instance declarations
376
       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
377

378 379 380
       ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
             fam_insts   = concat fam_insts_s
             local_infos = concat local_infos_s
381

382 383 384
       ; gbl_env <- addClsInsts local_infos $
                    addFamInsts fam_insts   $
                    getGblEnv
385

386 387 388 389 390 391 392 393 394
       ; 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]
395 396 397
  -> [LTyClDecl GhcRn]
  -> [LDerivDecl GhcRn]
  -> TcM (TcGblEnv, [InstInfo GhcRn], HsValBinds GhcRn)
398 399 400 401 402 403 404 405 406
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) }
407

408
addClsInsts :: [InstInfo GhcRn] -> TcM a -> TcM a
409
addClsInsts infos thing_inside
410
  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
411

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

Austin Seipp's avatar
Austin Seipp committed
429
{-
430 431 432 433 434 435 436 437
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)
438 439
the scoping of the generated code inside the bracket does not seem to
work out.
440 441 442

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

447 448
tcLocalInstDecl :: LInstDecl GhcRn
                -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
Ian Lynagh's avatar
Ian Lynagh committed
449 450 451 452
        -- A source-file instance declaration
        -- Type-check all the stuff before the "where"
        --
        -- We check for respectable instance type, and context
453
tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
454
  = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
455
       ; return ([], [fam_inst], []) }
456

457
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
458 459
  = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl Nothing (L loc decl)
       ; return ([], [fam_inst], maybeToList m_deriv_info) }
460 461

tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
462 463
  = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
       ; return (insts, fam_insts, deriv_infos) }
464

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

479
        -- Next, process any associated types.
480
        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
481 482
        ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
                           mapAndRecoverM (tcTyFamInstDecl mb_info) ats
483
        ; datafam_stuff <- tcExtendTyVarEnv tyvars $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
484
                           mapAndRecoverM (tcDataFamInstDecl mb_info) adts
485 486
        ; let (datafam_insts, m_deriv_infos) = unzip datafam_stuff
              deriv_infos                    = catMaybes m_deriv_infos
487

dreixel's avatar
dreixel committed
488
        -- Check for missing associated types and build them
489
        -- from their defaults (if available)
490
        ; let defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
491
                            `unionNameSet`
492 493 494 495
                            mkNameSet (map (unLoc . feqn_tycon
                                                  . hsib_body
                                                  . dfid_eqn
                                                  . unLoc) adts)
496
        ; tyfam_insts1 <- mapM (tcATDefault loc mini_subst defined_ats)
497
                               (classATItems clas)
498

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

504 505
        ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name tyvars theta
                              clas inst_tys
506

507
        ; let inst_info = InstInfo { iSpec  = ispec
508 509
                                   , iBinds = InstBindings
                                     { ib_binds = binds
510
                                     , ib_tyvars = map Var.varName tyvars -- Scope over bindings
511
                                     , ib_pragmas = uprags
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
512
                                     , ib_extensions = []
513
                                     , ib_derived = False } }
514

515 516
        ; doClsInstErrorChecks inst_info

517 518
        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts
                 , deriv_infos ) }
519

520

521
doClsInstErrorChecks :: InstInfo GhcRn -> TcM ()
522 523 524 525 526 527 528 529
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

530 531 532 533
         -- If not in an hs-boot file, abstract classes cannot have
         -- instances declared
      ; failIfTc (not is_boot && isAbstractClass clas) abstractClassInstErr

534 535 536 537
         -- Handwritten instances of any rejected
         -- class is always forbidden
         -- #12837
      ; failIfTc (clas_nm `elem` rejectedClassNames) clas_err
538 539 540 541 542 543 544 545 546 547 548

         -- 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
549
    clas     = is_cls ispec
550 551 552 553 554 555

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

556 557 558
    abstractClassInstErr =
        text "Cannot define instance for abstract class" <+> quotes (ppr clas_nm)

559
    -- Report an error or a warning for certain class instances.
560 561 562
    -- 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.
563 564 565 566
    rejectedClassNames = [ typeableClassName
                         , knownNatClassName
                         , knownSymbolClassName ]
    clas_err = text "Class" <+> quotes (ppr clas_nm)
567 568
                    <+> text "does not support user-specified instances"

Austin Seipp's avatar
Austin Seipp committed
569 570 571
{-
************************************************************************
*                                                                      *
572
               Type checking family instances
Austin Seipp's avatar
Austin Seipp committed
573 574
*                                                                      *
************************************************************************
575 576 577 578 579

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
580
-}
581

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

600
       ; return fam_tc }
601

602
tcTyFamInstDecl :: Maybe ClsInstInfo
603
                -> LTyFamInstDecl GhcRn -> TcM FamInst
604
  -- "type instance"
605
tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
606 607
  = setSrcSpan loc           $
    tcAddTyFamInstCtxt decl  $
608
    do { let fam_lname = feqn_tycon (hsib_body eqn)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
609 610 611
       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname

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

616
         -- (1) do the work of verifying the synonym group
617
       ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo
618
                                        (L (getLoc fam_lname) eqn)
619

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

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

628
tcDataFamInstDecl :: Maybe ClsInstInfo
629
                  -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
630
  -- "newtype instance" and "data instance"
631
tcDataFamInstDecl mb_clsinfo
632 633 634 635 636 637 638 639 640 641 642
    (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_vars = tv_names
                                                   , hsib_body =
      FamEqn { feqn_pats   = pats
             , feqn_tycon  = fam_tc_name
             , feqn_fixity = fixity
             , feqn_rhs    = HsDataDefn { dd_ND = new_or_data
                                        , dd_cType = cType
                                        , dd_ctxt = ctxt
                                        , dd_cons = cons
                                        , dd_kindSig = m_ksig
                                        , dd_derivs = derivs } }}}))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
643 644 645 646 647 648
  = 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)
649
       ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
650

dreixel's avatar
dreixel committed
651
         -- Kind check type patterns
652
       ; let mb_kind_env = thdOf3 <$> mb_clsinfo
653
       ; tcFamTyPats fam_tc mb_clsinfo tv_names pats
654
                     (kcDataDefn mb_kind_env decl) $
655 656
             \tvs pats res_kind ->
    do { stupid_theta <- solveEqualities $ tcHsContext ctxt
657

658 659 660 661 662
            -- Zonk the patterns etc into the Type world
       ; (ze, tvs')    <- zonkTyBndrsX emptyZonkEnv tvs
       ; pats'         <- zonkTcTypeToTypes ze pats
       ; res_kind'     <- zonkTcTypeToType  ze res_kind
       ; stupid_theta' <- zonkTcTypeToTypes ze stupid_theta
663

664
       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta' cons
665

dreixel's avatar
dreixel committed
666
         -- Construct representation tycon
667
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
668
       ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
669

670 671
       ; let (eta_pats, etad_tvs) = eta_reduce pats'
             eta_tvs              = filterOut (`elem` etad_tvs) tvs'
672 673
                 -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced

Simon Peyton Jones's avatar
Simon Peyton Jones committed
674
             full_tcbs = mkTyConBindersPreferAnon (eta_tvs ++ etad_tvs) res_kind'
675 676 677 678
                 -- 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)
679

Simon Peyton Jones's avatar
Simon Peyton Jones committed
680 681 682 683 684 685 686 687
         -- Deal with any kind signature.
         -- See also Note [Arity of data families] in FamInstEnv
       ; (extra_tcbs, final_res_kind) <- tcDataKindSig full_tcbs res_kind'
       ; checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind')

       ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
             all_pats    = pats' `chkAppend` extra_pats
             orig_res_ty = mkTyConApp fam_tc all_pats
688

689
       ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
690
           do { let ty_binders = full_tcbs `chkAppend` extra_tcbs
691
              ; data_cons <- tcConDecls rec_rep_tc
692
                                        (ty_binders, orig_res_ty) cons
693 694 695 696
              ; 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)
697
              -- freshen tyvars
698
              ; let axiom  = mkSingleCoAxiom Representational
699
                                             axiom_name eta_tvs [] fam_tc eta_pats
700
                                             (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
701
                    parent = DataFamInstTyCon axiom fam_tc all_pats
702

703

704
                      -- NB: Use the full ty_binders from the pats. See bullet toward
705
                      -- the end of Note [Data type families] in TyCon
706
                    rep_tc   = mkAlgTyCon rep_tc_name
707
                                          ty_binders liftedTypeKind
708
                                          (map (const Nominal) ty_binders)
709 710
                                          (fmap unLoc cType) stupid_theta
                                          tc_rhs parent
Edward Z. Yang's avatar
Edward Z. Yang committed
711
                                          gadt_syntax
712 713 714 715 716
                 -- 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.
717
              ; return (rep_tc, axiom) }
718 719

         -- Remember to check validity; no recursion to worry about here
720 721
         -- Check that left-hand sides are ok (mono-types, no type families,
         -- consistent instantiations, etc)
722
       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats' extra_pats pp_hs_pats
723 724

         -- Result kind must be '*' (otherwise, we have too few patterns)
725
       ; checkTc (isLiftedTypeKind final_res_kind) $
726 727
         tooFewParmsErr (tyConArity fam_tc)

728
       ; checkValidTyCon rep_tc
729 730

       ; let m_deriv_info = case derivs of
Ryan Scott's avatar
Ryan Scott committed
731 732 733 734 735
               L _ []    -> Nothing
               L _ preds ->
                 Just $ DerivInfo { di_rep_tc  = rep_tc
                                  , di_clauses = preds
                                  , di_ctxt    = tcMkDataFamInstCtxt decl }
736

737
       ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
738
       ; return (fam_inst, m_deriv_info) } }
739
  where
740 741 742 743 744 745 746 747 748 749 750
    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
751
      , not (tv `elemVarSet` tyCoVarsOfTypes pats)
752 753
      = go pats (tv : etad_tvs)
    go pats etad_tvs = (reverse pats, etad_tvs)
754

755
    pp_hs_pats = pprFamInstLHS fam_tc_name pats fixity (unLoc ctxt) m_ksig
756

757
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
758
*                                                                      *
759
      Type-checking instance declarations, pass 2
Austin Seipp's avatar
Austin Seipp committed
760
*                                                                      *
761
********************************************************************* -}
762

763 764
tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn]
             -> TcM (LHsBinds GhcTc)
Ian Lynagh's avatar
Ian Lynagh committed
765 766
-- (a) From each class declaration,
--      generate any default-method bindings
767
-- (b) From each instance decl
Ian Lynagh's avatar
Ian Lynagh committed
768
--      generate the dfun binding
769 770

tcInstDecls2 tycl_decls inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
771
  = do  { -- (a) Default methods from class decls
772
          let class_decls = filter (isClassDecl . unLoc) tycl_decls
773
        ; dm_binds_s <- mapM tcClassDecl2 class_decls
774
        ; let dm_binds = unionManyBags dm_binds_s
dterei's avatar
dterei committed
775

Ian Lynagh's avatar
Ian Lynagh committed
776
          -- (b) instance declarations
dterei's avatar
dterei committed
777 778
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
779
              -- (they were arready added in TcTyDecls.tcAddImplicits)
780
              -- See Note [Default methods in the type environment]
781
        ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
782
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
783 784

          -- Done
785
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
786

787 788
{- Note [Default methods in the type environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
789
The default method Ids are already in the type environment (see Note
790
[Default method Ids and Template Haskell] in TcTyDcls), BUT they
791 792 793 794 795 796
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).

797
So right here in tcInstDecls2 we must re-extend the type envt with
798
the default method Ids replete with their INLINE pragmas.  Urk.
Austin Seipp's avatar
Austin Seipp committed
799
-}
800

801
tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
802 803 804 805
            -- Returns a binding for the dfun
tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
  = recoverM (return emptyLHsBinds)             $
    setSrcSpan loc                              $
dterei's avatar
dterei committed
806
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
807
    do {  -- Instantiate the instance decl with skolem constants
808
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
809
       ; dfun_ev_vars <- newEvVars dfun_theta
dimitris's avatar
dimitris committed
810 811 812
                     -- We instantiate the dfun_id with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
813

814
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
815
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
niteria's avatar
niteria committed
816
             sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
817

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

820 821
                      -- Deal with 'SPECIALISE instance' pragmas
                      -- See Note [SPECIALISE instance pragmas]
822
       ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
823

824 825 826 827 828 829
         -- 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 $
830
                do { (sc_ids, sc_binds, sc_implics)
831
                        <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
832
                                          inst_tys dfun_ev_binds
833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849
                                          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
850
                                  , ic_wanted = mkImplicWC sc_meth_implics