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

66
import Control.Monad
67
import Maybes
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
  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
147
  df_i, leaving a *self*-recursive op1_i.  (If op1_i doesn't call op at
148
  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
   :: [LInstDecl Name]          -- Source code instance decls
Ian Lynagh's avatar
Ian Lynagh committed
364
   -> TcM (TcGblEnv,            -- The full inst env
365
           [InstInfo Name],     -- Source-code instance decls to process;
Ian Lynagh's avatar
Ian Lynagh committed
366
                                -- contains all dfuns for this module
367
           [DerivInfo])         -- From data family instances
368

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

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

377 378 379
       ; gbl_env <- addClsInsts local_infos $
                    addFamInsts fam_insts   $
                    getGblEnv
380

381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401
       ; 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) }
402

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

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

Austin Seipp's avatar
Austin Seipp committed
424
{-
425 426 427 428 429 430 431 432
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)
433 434
the scoping of the generated code inside the bracket does not seem to
work out.
435 436 437

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

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

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

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

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

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

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

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

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

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

507 508
        ; doClsInstErrorChecks inst_info

509 510
        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts
                 , deriv_infos ) }
511

512

513 514 515 516 517 518 519 520 521
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

522 523 524 525
         -- Handwritten instances of any rejected
         -- class is always forbidden
         -- #12837
      ; failIfTc (clas_nm `elem` rejectedClassNames) clas_err
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542

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

543
    -- Report an error or a warning for certain class instances.
544 545 546
    -- 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.
547 548 549 550
    rejectedClassNames = [ typeableClassName
                         , knownNatClassName
                         , knownSymbolClassName ]
    clas_err = text "Class" <+> quotes (ppr clas_nm)
551 552
                    <+> text "does not support user-specified instances"

Austin Seipp's avatar
Austin Seipp committed
553 554 555
{-
************************************************************************
*                                                                      *
556
               Type checking family instances
Austin Seipp's avatar
Austin Seipp committed
557 558
*                                                                      *
************************************************************************
559 560 561 562 563

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
564
-}
565

566
tcFamInstDeclCombined :: Maybe ClsInstInfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
567 568
                      -> Located Name -> TcM TyCon
tcFamInstDeclCombined mb_clsinfo fam_tc_lname
569
  = do { -- Type family instances require -XTypeFamilies
570
         -- and can't (currently) be in an hs-boot file
571
       ; traceTc "tcFamInstDecl" (ppr fam_tc_lname)
572
       ; type_families <- xoptM LangExt.TypeFamilies
573
       ; is_boot <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
574 575 576 577 578 579
       ; 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
580 581
       ; when (isNothing mb_clsinfo &&   -- Not in a class decl
               isTyConAssoc fam_tc)      -- but an associated type
582 583
              (addErr $ assocInClassErr fam_tc_lname)

584
       ; return fam_tc }
585

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

         -- (0) Check it's an open type family
Jan Stolarek's avatar
Jan Stolarek committed
596 597
       ; checkTc (isFamilyTyCon fam_tc)         (notFamily fam_tc)
       ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
598
       ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
599

600
         -- (1) do the work of verifying the synonym group
601
       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) mb_clsinfo eqn
602

603
         -- (2) check for validity
Jan Stolarek's avatar
Jan Stolarek committed
604
       ; checkValidCoAxBranch mb_clsinfo fam_tc co_ax_branch
605

606
         -- (3) construct coercion axiom
607
       ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
608 609
       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
       ; newFamInst SynFamilyInst axiom }
610

611
tcDataFamInstDecl :: Maybe ClsInstInfo
612
                  -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo)
613
  -- "newtype instance" and "data instance"
614
tcDataFamInstDecl mb_clsinfo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
615 616 617 618
    (L loc decl@(DataFamInstDecl
       { dfid_pats = pats
       , dfid_tycon = fam_tc_name
       , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
619 620
                                     , dd_ctxt = ctxt, dd_cons = cons
                                     , dd_derivs = derivs } }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
621 622 623 624 625 626
  = 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)
627
       ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
628

dreixel's avatar
dreixel committed
629
         -- Kind check type patterns
630
       ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
631
                     (kcDataDefn (unLoc fam_tc_name) pats defn) $
632 633
             \tvs pats res_kind ->
    do { stupid_theta <- solveEqualities $ tcHsContext ctxt
634

635 636 637 638 639
            -- 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
640

641
       ; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta' cons
642

dreixel's avatar
dreixel committed
643
         -- Construct representation tycon
644
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
645
       ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
646

647 648 649 650 651 652 653 654
       ; 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'
655

656
       ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
657
           do { let ty_binders = mkTyConBindersPreferAnon full_tvs liftedTypeKind
658
              ; data_cons <- tcConDecls rec_rep_tc
659
                                        (ty_binders, orig_res_ty) cons
660 661 662 663
              ; 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)
664
              -- freshen tyvars
665
              ; let axiom  = mkSingleCoAxiom Representational
666
                                             axiom_name eta_tvs [] fam_tc eta_pats
667 668
                                             (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                    parent = DataFamInstTyCon axiom fam_tc pats'
669

670 671

                      -- NB: Use the full_tvs from the pats. See bullet toward
672
                      -- the end of Note [Data type families] in TyCon
673
                    rep_tc   = mkAlgTyCon rep_tc_name
674
                                          ty_binders liftedTypeKind
675 676 677
                                          (map (const Nominal) full_tvs)
                                          (fmap unLoc cType) stupid_theta
                                          tc_rhs parent
Edward Z. Yang's avatar
Edward Z. Yang committed
678
                                          gadt_syntax
679 680 681 682 683
                 -- 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.
684
              ; return (rep_tc, axiom) }
685 686

         -- Remember to check validity; no recursion to worry about here
687 688 689 690 691 692 693 694
         -- Check that left-hand sides are ok (mono-types, no type families,
         -- consistent instantiations, etc)
       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'

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

695
       ; checkValidTyCon rep_tc
696 697

       ; let m_deriv_info = case derivs of
Ryan Scott's avatar
Ryan Scott committed
698 699 700 701 702
               L _ []    -> Nothing
               L _ preds ->
                 Just $ DerivInfo { di_rep_tc  = rep_tc
                                  , di_clauses = preds
                                  , di_ctxt    = tcMkDataFamInstCtxt decl }
703

704
       ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
705
       ; return (fam_inst, m_deriv_info) } }
706
  where
707 708 709 710 711 712 713 714 715 716 717
    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
718
      , not (tv `elemVarSet` tyCoVarsOfTypes pats)
719 720
      = go pats (tv : etad_tvs)
    go pats etad_tvs = (reverse pats, etad_tvs)
721

722

723
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
724
*                                                                      *
725
      Type-checking instance declarations, pass 2
Austin Seipp's avatar
Austin Seipp committed
726
*                                                                      *
727
********************************************************************* -}
728

729
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
730
             -> TcM (LHsBinds Id)
Ian Lynagh's avatar
Ian Lynagh committed
731 732
-- (a) From each class declaration,
--      generate any default-method bindings
733
-- (b) From each instance decl
Ian Lynagh's avatar
Ian Lynagh committed
734
--      generate the dfun binding
735 736

tcInstDecls2 tycl_decls inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
737
  = do  { -- (a) Default methods from class decls
738
          let class_decls = filter (isClassDecl . unLoc) tycl_decls
739
        ; dm_binds_s <- mapM tcClassDecl2 class_decls
740
        ; let dm_binds = unionManyBags dm_binds_s
dterei's avatar
dterei committed
741

Ian Lynagh's avatar
Ian Lynagh committed
742
          -- (b) instance declarations
dterei's avatar
dterei committed
743 744
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
745
              -- (they were arready added in TcTyDecls.tcAddImplicits)
746
              -- See Note [Default methods in the type environment]
747
        ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
748
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
749 750

          -- Done
751
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
752

753 754
{- Note [Default methods in the type environment]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755
The default method Ids are already in the type environment (see Note
756
[Default method Ids and Template Haskell] in TcTyDcls), BUT they
757 758 759 760 761 762
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).

763
So right here in tcInstDecls2 we must re-extend the type envt with
764
the default method Ids replete with their INLINE pragmas.  Urk.
Austin Seipp's avatar
Austin Seipp committed
765
-}
766

767 768 769 770 771
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
772
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
773
    do {  -- Instantiate the instance decl with skolem constants
774
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
775
       ; dfun_ev_vars <- newEvVars dfun_theta
dimitris's avatar
dimitris committed
776 777 778
                     -- We instantiate the dfun_id with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
779

780
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
781
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
niteria's avatar
niteria committed
782
             sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
783

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

786 787
                      -- Deal with 'SPECIALISE instance' pragmas
                      -- See Note [SPECIALISE instance pragmas]
788
       ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
789

790 791 792 793 794 795
         -- 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 $
796
                do { (sc_ids, sc_binds, sc_implics)
797
                        <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
798
                                          inst_tys dfun_ev_binds
799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815
                                          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
816
                                  , ic_wanted = mkImplicWC sc_meth_implics
817
                                  , ic_status = IC_Unsolved
818
                                  , ic_binds  = dfun_ev_binds_var
819
                                  , ic_needed = emptyVarSet
820 821
                                  , ic_env    = env
                                  , ic_info   = InstSkol }
822

823
       -- Create the result bindings
batterseapower's avatar
batterseapower committed
824
       ; self_dict <- newDict clas inst_tys
825 826
       ; let class_tc      = classTyCon clas
             [dict_constr] = tyConDataCons class_tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
827 828
             dict_bind     = mkVarBind self_dict (L loc con_app_args)

829 830 831 832
                     -- 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
833
                     -- member) are dealt with by the common MkId.mkDataConWrapId
dterei's avatar
dterei committed
834 835 836 837
                     -- code rather than needing to be repeated here.
                     --    con_app_tys  = MkD ty1 ty2
                     --    con_app_scs  = MkD ty1 ty2 sc1 sc2
                     --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
838
             con_app_tys  = wrapId (mkWpTyApps inst_tys) (dataConWrapId dict_constr)
839 840 841
                       -- NB: We *can* have covars in inst_tys, in the case of
                       -- promoted GADT constructors.

842
             con_app_args = foldl app_to_meth con_app_tys sc_meth_ids
Simon Peyton Jones's avatar
Simon Peyton Jones committed
843

844 845
             app_to_meth :: HsExpr Id -> Id -> HsExpr Id
             app_to_meth fun meth_id = L loc fun `HsApp` L loc (wrapId arg_wrapper meth_id)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
846

847
             inst_tv_tys = mkTyVarTys inst_tyvars
Simon Peyton Jones's avatar
Simon Peyton Jones committed
848
             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
849

850
             is_newtype = isNewTyCon class_tc
851
             dfun_id_w_prags = addDFunPrags dfun_id sc_meth_ids
852
             dfun_spec_prags
853 854
                | is_newtype = SpecPrags []
                | otherwise  = SpecPrags spec_inst_prags
855 856 857
                    -- Newtype dfuns just inline unconditionally,
                    -- so don't attempt to specialise them