TcInstDcls.lhs 64 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
%
5
6

TcInstDecls: Typechecking instance declarations
7
8

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
9
10
11
12
13
14
15
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

16
module TcInstDcls ( tcInstDecls1, tcInstDecls2 ) where
17

dterei's avatar
dterei committed
18
19
#include "HsVersions.h"

20
import HsSyn
21
import TcBinds
22
import TcTyClsDecls
23
24
25
import TcClassDcl( tcClassDecl2, 
                   HsSigFun, lookupHsSig, mkHsSigFun, emptyHsSigs,
                   findMethodBind, instantiateMethod, tcInstanceMethodBody )
dterei's avatar
dterei committed
26
import TcPat      ( addInlinePrags )
Ian Lynagh's avatar
Ian Lynagh committed
27
import TcRnMonad
28
import TcValidity
29
30
import TcMType
import TcType
31
import BuildTyCl
32
33
34
35
36
37
38
39
import Inst
import InstEnv
import FamInst
import FamInstEnv
import TcDeriv
import TcEnv
import TcHsType
import TcUnify
dterei's avatar
dterei committed
40
import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
41
import Type
42
import TcEvidence
43
import TyCon
44
import CoAxiom
45
46
47
import DataCon
import Class
import Var
48
import VarEnv
49
import VarSet 
50
import Pair
51
import CoreUnfold ( mkDFunUnfolding )
52
import CoreSyn    ( Expr(Var, Type), CoreExpr, mkTyApps, mkVarApps )
53
import PrelNames  ( tYPEABLE_INTERNAL, typeableClassName, oldTypeableClassNames )
dterei's avatar
dterei committed
54
55
56
57

import Bag
import BasicTypes
import DynFlags
58
import ErrUtils
dterei's avatar
dterei committed
59
import FastString
60
import HscTypes ( isHsBoot )
61
import Id
62
63
64
import MkId
import Name
import NameSet
65
import NameEnv
dterei's avatar
dterei committed
66
import Outputable
67
68
import SrcLoc
import Util
dterei's avatar
dterei committed
69

70
import Control.Monad
Simon Peyton Jones's avatar
Simon Peyton Jones committed
71
import Maybes     ( orElse, isNothing )
72
73
74
\end{code}

Typechecking instance declarations is done in two passes. The first
75
76
pass, made by @tcInstDecls1@, collects information to be used in the
second pass.
77
78
79
80
81
82
83

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.

84
85
86
87
88
89

Note [How instance declarations are translated]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here is how we translation instance declarations into Core

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

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

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

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

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

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

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

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

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

189
190
191
 * 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
192

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

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

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

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

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

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

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

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

221
Instead, we simply rely on the fact that casts are cheap:
222

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

228
229
   $cop_list :: forall a. C a => [a] -> [a]
   $cop_list = <blah>
230

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

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

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

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

263
264
    class DeepSeq a where
      deepSeq :: a -> b -> b
265

266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
    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
293

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

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
309
instance.
310

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

329
330
331
332
333
334
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.

335

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

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

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

354

355
356

%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
357
%*                                                                      *
358
\subsection{Extracting instance decls}
Ian Lynagh's avatar
Ian Lynagh committed
359
%*                                                                      *
360
361
362
363
%************************************************************************

Gather up the instance declarations from their various sources

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

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

380
            -- Do class and family instance declarations
381
       ; env <- getGblEnv
382
383
       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
       ; let (local_infos_s, fam_insts_s) = unzip stuff
384
385
386
387
388
             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
             (typeable_instances, local_infos) = splitTypeable env local_infos'
389

390
391
       ; addClsInsts local_infos $
         addFamInsts fam_insts   $
392
    do {    -- Compute instances from "deriving" clauses;
393
394
395
396
            -- 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
397
         failIfErrsM    -- If the addInsts stuff gave any errors, don't
dterei's avatar
dterei committed
398
399
                        -- try the deriving stuff, because that may give
                        -- more errors still
dreixel's avatar
dreixel committed
400

401
       ; traceTc "tcDeriving" empty
402
       ; th_stage <- getStage   -- See Note [Deriving inside TH brackets ]
403
       ; (gbl_env, deriv_inst_info, deriv_binds)
404
              <- if isBrackStage th_stage 
405
406
                 then do { gbl_env <- getGblEnv
                         ; return (gbl_env, emptyBag, emptyValBindsOut) }
407
408
                 else tcDeriving tycl_decls inst_decls deriv_decls

409
410
411
       -- Remove any handwritten instance of poly-kinded Typeable and warn
       ; dflags <- getDynFlags
       ; when (wopt Opt_WarnTypeableInstances dflags) $
412
              mapM_ (failWithTc . instMsg) typeable_instances
413

414
       -- Check that if the module is compiled with -XSafe, there are no
415
       -- hand written instances of old Typeable as then unsafe casts could be
dreixel's avatar
dreixel committed
416
       -- performed. Derived instances are OK.
417
       ; when (safeLanguageOn dflags) $
418
             mapM_ (\x -> when (typInstCheck x)
419
                               (addErrAt (getSrcSpan $ iSpec x) typInstErr))
420
                   local_infos
421
422
       -- As above but for Safe Inference mode.
       ; when (safeInferOn dflags) $
423
             mapM_ (\x -> when (typInstCheck x) recordUnsafeInfer) local_infos
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
431
432
433
434
435
436
437
438
439
440
441
442
443
    -- Separate the Typeable instances from the rest
    splitTypeable _   []     = ([],[])
    splitTypeable env (i:is) =
      let (typeableInsts, otherInsts) = splitTypeable env is
      in if -- We will filter out instances of Typeable
            (typeableClassName == is_cls_nm (iSpec i))
            -- but not those that come from Data.Typeable.Internal
            && tcg_mod env /= tYPEABLE_INTERNAL
            -- nor those from an .hs-boot file (deriving can't be used there)
            && not (isHsBoot (tcg_src env))
         then (i:typeableInsts, otherInsts)
         else (typeableInsts, i:otherInsts)

    typInstCheck ty = is_cls_nm (iSpec ty) `elem` oldTypeableClassNames
dterei's avatar
dterei committed
444
445
    typInstErr = ptext $ sLit $ "Can't create hand written instances of Typeable in Safe"
                              ++ " Haskell! Can only derive them"
446

447
    instMsg i = hang (ptext (sLit $ "Typeable instances can only be derived; replace "
448
449
450
                                 ++ "the following instance:"))
                     2 (pprInstance (iSpec i))

451
452
addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
addClsInsts infos thing_inside
453
  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
454

455
addFamInsts :: [FamInst] -> TcM a -> TcM a
456
457
458
459
-- Extend (a) the family instance envt
--        (b) the type envt with stuff from data type decls
addFamInsts fam_insts thing_inside
  = tcExtendLocalFamInstEnv fam_insts $ 
460
    tcExtendGlobalEnv things  $ 
461
462
    do { traceTc "addFamInsts" (pprFamInsts fam_insts)
       ; tcg_env <- tcAddImplicits things
463
464
       ; setGblEnv tcg_env thing_inside }
  where
465
    axioms = map (toBranchedAxiom . famInstAxiom) fam_insts
466
467
    tycons = famInstsRepTyCons fam_insts
    things = map ATyCon tycons ++ map ACoAxiom axioms 
468
\end{code}
469

470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
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)
the scoping of the generated code inside the bracket does not seem to 
work out.  

The easy solution is simply not to generate the derived instances at
all.  (A less brutal solution would be to generate them with no
bindings.)  This will become moot when we shift to the new TH plan, so 
the brutal solution will do.


487
\begin{code}
488
tcLocalInstDecl :: LInstDecl Name
489
                -> TcM ([InstInfo Name], [FamInst])
Ian Lynagh's avatar
Ian Lynagh committed
490
491
492
493
        -- A source-file instance declaration
        -- Type-check all the stuff before the "where"
        --
        -- We check for respectable instance type, and context
494
tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
495
  = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
496
497
       ; return ([], [fam_inst]) }

498
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
499
  = do { fam_inst <- tcDataFamInstDecl Nothing (L loc decl)
500
       ; return ([], [fam_inst]) }
501
502

tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
503
  = do { (insts, fam_insts) <- tcClsInstDecl (L loc decl)
504
       ; return (insts, fam_insts) }
505

506
tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst])
Simon Peyton Jones's avatar
Simon Peyton Jones committed
507
508
509
510
511
tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                  , cid_sigs = uprags, cid_tyfam_insts = ats
                                  , cid_datafam_insts = adts }))
  = setSrcSpan loc                      $
    addErrCtxt (instDeclCtxt1 poly_ty)  $
Ian Lynagh's avatar
Ian Lynagh committed
512
513
514
515
    do  { is_boot <- tcIsHsBoot
        ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
                  badBootDeclErr

dreixel's avatar
dreixel committed
516
        ; (tyvars, theta, clas, inst_tys) <- tcHsInstHead InstDeclCtxt poly_ty
517
518
        ; let mini_env   = mkVarEnv (classTyVars clas `zip` inst_tys)
              mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env
Simon Peyton Jones's avatar
Simon Peyton Jones committed
519
              mb_info    = Just (clas, mini_env)
520
                           
521
        -- Next, process any associated types.
522
        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
523
        ; tyfam_insts0 <- tcExtendTyVarEnv tyvars $
524
                          mapAndRecoverM (tcAssocTyDecl clas mini_env) ats
525
        ; datafam_insts <- tcExtendTyVarEnv tyvars $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
526
                           mapAndRecoverM (tcDataFamInstDecl mb_info) adts
527

dreixel's avatar
dreixel committed
528
        -- Check for missing associated types and build them
529
        -- from their defaults (if available)
530
531
        ; let defined_ats = mkNameSet $ map (tyFamInstDeclName . unLoc) ats
              defined_adts = mkNameSet $ map (unLoc . dfid_tycon . unLoc) adts
532

533
              mk_deflt_at_instances :: ClassATItem -> TcM [FamInst]
534
              mk_deflt_at_instances (fam_tc, defs)
535
                 -- User supplied instances ==> everything is OK
536
537
                | tyConName fam_tc `elemNameSet` defined_ats
                   || tyConName fam_tc `elemNameSet` defined_adts
538
539
                = return []

540
                 -- No defaults ==> generate a warning
541
542
543
544
                | null defs
                = do { warnMissingMethodOrAT "associated type" (tyConName fam_tc)
                     ; return [] }

545
                 -- No user instance, have defaults ==> instatiate them
546
547
548
549
                 -- Example:   class C a where { type F a b :: *; type F a b = () }
                 --            instance C [x]
                 -- Then we want to generate the decl:   type F [x] b = ()
                | otherwise 
550
                = forM defs $ \(CoAxBranch { cab_lhs = pat_tys, cab_rhs = rhs }) ->
551
552
553
554
555
                  do { let pat_tys' = substTys mini_subst pat_tys
                           rhs'     = substTy  mini_subst rhs
                           tv_set'  = tyVarsOfTypes pat_tys'
                           tvs'     = varSetElems tv_set'
                     ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
556
                     ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
557
                     ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
558
                       newFamInst SynFamilyInst axiom }
559

560
        ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
561
        
Ian Lynagh's avatar
Ian Lynagh committed
562
563
        -- Finally, construct the Core representation of the instance.
        -- (This no longer includes the associated types.)
564
        ; dfun_name <- newDFunName clas inst_tys (getLoc poly_ty)
dterei's avatar
dterei committed
565
                -- Dfun location is that of instance *header*
566

Ian Lynagh's avatar
Ian Lynagh committed
567
        ; overlap_flag <- getOverlapFlag
568
        ; (subst, tyvars') <- tcInstSkolTyVars tyvars
569
        ; let dfun  	= mkDictFunId dfun_name tyvars theta clas inst_tys
570
571
572
              ispec 	= mkLocalInstance dfun overlap_flag tyvars' clas (substTys subst inst_tys)
                            -- Be sure to freshen those type variables, 
                            -- so they are sure not to appear in any lookup
573
574
              inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }

575
        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
576
577
578
579
580

--------------
tcAssocTyDecl :: Class                   -- Class of associated type
              -> VarEnv Type             -- Instantiation of class TyVars
              -> LTyFamInstDecl Name     
581
              -> TcM (FamInst)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
582
583
tcAssocTyDecl clas mini_env ldecl
  = do { fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) ldecl
584
       ; return fam_inst }
585
586
\end{code}

587
588
589
590
591
592
593
594
595
596
597
598
%************************************************************************
%*                                                                      *
               Type checking family instances
%*                                                                      *
%************************************************************************

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

\begin{code}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
599
600
601
tcFamInstDeclCombined :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
                      -> Located Name -> TcM TyCon
tcFamInstDeclCombined mb_clsinfo fam_tc_lname
602
  = do { -- Type family instances require -XTypeFamilies
603
         -- and can't (currently) be in an hs-boot file
604
       ; traceTc "tcFamInstDecl" (ppr fam_tc_lname)
605
606
607
608
609
610
611
612
       ; type_families <- xoptM Opt_TypeFamilies
       ; is_boot <- tcIsHsBoot   -- Are we compiling an hs-boot file?
       ; 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
613
614
       ; when (isNothing mb_clsinfo &&   -- Not in a class decl
               isTyConAssoc fam_tc)      -- but an associated type
615
616
              (addErr $ assocInClassErr fam_tc_lname)

617
       ; return fam_tc }
618

619
tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
620
                -> LTyFamInstDecl Name -> TcM FamInst
621
  -- "type instance"
622
tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
623
624
  = setSrcSpan loc           $
    tcAddTyFamInstCtxt decl  $
625
    do { let fam_lname = tfie_tycon (unLoc eqn)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
626
627
628
629
       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname

         -- (0) Check it's an open type family
       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
630
631
       ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
       ; checkTc (isOpenSynFamilyTyCon fam_tc)
632
633
                 (notOpenFamily fam_tc)

634
         -- (1) do the work of verifying the synonym group
635
       ; co_ax_branch <- tcSynFamInstDecl fam_tc decl
636

637
638
         -- (2) check for validity
       ; checkValidTyFamInst mb_clsinfo fam_tc co_ax_branch
639

640
         -- (3) construct coercion axiom
641
642
       ; rep_tc_name <- newFamInstAxiomName loc
                                            (tyFamInstDeclName decl)
643
644
645
                                            [co_ax_branch]
       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
       ; newFamInst SynFamilyInst axiom }
646

647
tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
648
                  -> LDataFamInstDecl Name -> TcM FamInst
649
  -- "newtype instance" and "data instance"
Simon Peyton Jones's avatar
Simon Peyton Jones committed
650
651
652
653
654
655
656
657
658
659
660
661
tcDataFamInstDecl mb_clsinfo 
    (L loc decl@(DataFamInstDecl
       { dfid_pats = pats
       , dfid_tycon = fam_tc_name
       , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                                     , dd_ctxt = ctxt, dd_cons = cons } }))
  = 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)
662
663
       ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)

dreixel's avatar
dreixel committed
664
         -- Kind check type patterns
665
666
       ; tcFamTyPats (unLoc fam_tc_name) (tyConKind fam_tc) pats
                     (kcDataDefn (unLoc fam_tc_name) defn) $ 
667
           \tvs' pats' res_kind -> do
668

669
       { -- Check that left-hand side contains no type family applications
dreixel's avatar
dreixel committed
670
         -- (vanilla synonyms are fine, though, and we checked for
671
672
673
         --  foralls earlier)
         checkValidFamPats fam_tc tvs' pats'
         -- Check that type patterns match class instance head, if any
674
       ; checkConsistentFamInst mb_clsinfo fam_tc tvs' pats'
dreixel's avatar
dreixel committed
675
676
         
         -- Result kind must be '*' (otherwise, we have too few patterns)
677
       ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
678

679
       ; stupid_theta <- tcHsContext ctxt
680
       ; h98_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
681

dreixel's avatar
dreixel committed
682
         -- Construct representation tycon
683
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
684
       ; axiom_name  <- newImplicitBinder rep_tc_name mkInstTyCoOcc
685
       ; let orig_res_ty = mkTyConApp fam_tc pats'
686
687

       ; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
688
           do { data_cons <- tcConDecls new_or_data (unLoc fam_tc_name) rec_rep_tc
dreixel's avatar
dreixel committed
689
                                       (tvs', orig_res_ty) cons
690
691
692
693
              ; 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)
694
              -- freshen tyvars
695
696
697
              ; let (eta_tvs, eta_pats) = eta_reduce tvs' pats'
                    axiom    = mkSingleCoAxiom axiom_name eta_tvs fam_tc eta_pats 
                                               (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
698
                    parent   = FamInstTyCon axiom fam_tc pats'
699
700
                    roles    = map (const Nominal) tvs'
                    rep_tc   = buildAlgTyCon rep_tc_name tvs' roles cType stupid_theta tc_rhs 
701
702
703
                                             Recursive 
                                             False      -- No promotable to the kind level
                                             h98_syntax parent
704
705
706
707
708
                 -- 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.
709
              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
710
711
712
              ; return (rep_tc, fam_inst) }

         -- Remember to check validity; no recursion to worry about here
713
714
       ; let role_annots = unitNameEnv rep_tc_name (repeat Nothing)
       ; checkValidTyCon rep_tc role_annots
715
       ; return fam_inst } }
716
717
718
719
720
721
722
723
724
725
  where
    -- See Note [Eta reduction for data family axioms]
    --  [a,b,c,d].T [a] c Int c d  ==>  [a,b,c]. T [a] c Int c
    eta_reduce tvs pats = go (reverse tvs) (reverse pats)
    go (tv:tvs) (pat:pats)
      | Just tv' <- getTyVar_maybe pat
      , tv == tv'
      , not (tv `elemVarSet` tyVarsOfTypes pats)
      = go tvs pats
    go tvs pats = (reverse tvs, reverse pats)
726
\end{code}
727

728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
Note [Eta reduction for data family axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
   data family T a b :: *
   newtype instance T Int a = MkT (IO a) deriving( Monad )
We'd like this to work.  From the 'newtype instance' you might
think we'd get:
   newtype TInt a = MkT (IO a)
   axiom ax1 a :: T Int a ~ TInt a   -- The type-instance part
   axiom ax2 a :: TInt a ~ IO a      -- The newtype part

But now what can we do?  We have this problem
   Given:   d  :: Monad IO
   Wanted:  d' :: Monad (T Int) = d |> ????
What coercion can we use for the ???

Solution: eta-reduce both axioms, thus:
   axiom ax1 :: T Int ~ TInt
   axiom ax2 :: TInt ~ IO
Now
   d' = d |> Monad (sym (ax2 ; ax1))

750
751
This eta reduction happens both for data instances and newtype instances.

752
753
754
755
See Note [Newtype eta] in TyCon.



756
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
757
%*                                                                      *
758
      Type-checking instance declarations, pass 2
Ian Lynagh's avatar
Ian Lynagh committed
759
%*                                                                      *
760
761
762
%************************************************************************

\begin{code}
763
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
764
             -> TcM (LHsBinds Id)
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
779
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
              -- See Note [Default methods and instances]
780
        ; inst_binds_s <- tcExtendLetEnv TopLevel dm_ids $
781
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
782
783

          -- Done
784
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
785
786
\end{code}

787
788
789
790
791
792
793
794
795
796
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).

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

800
\begin{code}
801
802
803
804
805
806

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
807
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
808
    do {  -- Instantiate the instance decl with skolem constants
809
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id)
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
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
814
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
815
             sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta
816

817
       ; dfun_ev_vars <- newEvVars dfun_theta
818

819
       ; (sc_binds, sc_ev_vars) <- tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta'
820
821
822

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

        -- Typecheck the methods
dterei's avatar
dterei committed
826
       ; (meth_ids, meth_binds)
827
828
829
830
831
           <- tcExtendTyVarEnv inst_tyvars $
                -- The inst_tyvars scope over the 'where' part
                -- Those tyvars are inside the dfun_id's type, which is a bit
                -- bizarre, but OK so long as you realise it!
              tcInstanceMethods dfun_id clas inst_tyvars dfun_ev_vars
832
                                inst_tys spec_inst_info
833
                                op_items ibinds
834

835
       -- Create the result bindings
batterseapower's avatar
batterseapower committed
836
       ; self_dict <- newDict clas inst_tys
837
838
       ; let class_tc      = classTyCon clas
             [dict_constr] = tyConDataCons class_tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
839
840
             dict_bind     = mkVarBind self_dict (L loc con_app_args)

841
842
843
844
                     -- 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
845
                     -- member) are dealt with by the common MkId.mkDataConWrapId
dterei's avatar
dterei committed
846
847
848
849
                     -- 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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
850
851
             con_app_tys  = wrapId (mkWpTyApps inst_tys)
                                   (dataConWrapId dict_constr)
852
             con_app_scs  = mkHsWrap (mkWpEvApps (map EvId sc_ev_vars)) con_app_tys
853
             con_app_args = foldl app_to_meth con_app_scs meth_ids
Simon Peyton Jones's avatar
Simon Peyton Jones committed
854

855
856
             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
857

858
             inst_tv_tys = mkTyVarTys inst_tyvars
Simon Peyton Jones's avatar
Simon Peyton Jones committed
859
             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
860

dterei's avatar
dterei committed
861
862
863
                -- Do not inline the dfun; instead give it a magic DFunFunfolding
                -- See Note [ClassOp/DFun selection]
                -- See also note [Single-method classes]
864
             (dfun_id_w_fun, dfun_spec_prags)
865
                | isNewTyCon class_tc
866
867
868
                = ( dfun_id `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
                  , SpecPrags [] )   -- Newtype dfuns just inline unconditionally,
                                     -- so don't attempt to specialise them
869
                | otherwise
870
871
872
873
                = ( dfun_id `setIdUnfolding`  mkDFunUnfolding (inst_tyvars ++ dfun_ev_vars)
                                                              dict_constr dfun_args
                            `setInlinePragma` dfunInlinePragma
                  , SpecPrags spec_inst_prags )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
874

875
876
877
878
879
             dfun_args :: [CoreExpr]
             dfun_args = map Type inst_tys        ++
                         map Var  sc_ev_vars      ++ 
                         map mk_meth_app meth_ids
             mk_meth_app meth_id = Var meth_id `mkTyApps` inst_tv_tys `mkVarApps` dfun_ev_vars 
880

881
             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id_w_fun
882
883
                          , abe_mono = self_dict, abe_prags = dfun_spec_prags }
                          -- NB: see Note [SPECIALISE instance pragmas]
884
             main_bind = AbsBinds { abs_tvs = inst_tyvars
885
                                  , abs_ev_vars = dfun_ev_vars
886
                                  , abs_exports = [export]
887
                                  , abs_ev_binds = sc_binds
888
                                  , abs_binds = unitBag dict_bind }
889

890
       ; return (unitBag (L loc main_bind) `unionBags`
891
                 listToBag meth_binds)
892
       }
893
 where
894
895
   dfun_id = instanceDFunId ispec
   loc     = getSrcSpan dfun_id
896

897
------------------------------
898
tcSuperClasses :: DFunId -> [TcTyVar] -> [EvVar] -> TcThetaType
899
               -> TcM (TcEvBinds, [EvVar])
900
901
902
903
904
905
906
907
-- See Note [Silent superclass arguments]
tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta
  = do {   -- Check that all superclasses can be deduced from
           -- the originally-specified dfun arguments
       ; (sc_binds, sc_evs) <- checkConstraints InstSkol inst_tyvars orig_ev_vars $
                               emitWanteds ScOrigin sc_theta

       ; if null inst_tyvars && null dfun_ev_vars 
908
909
         then return (sc_binds,       sc_evs)
         else return (emptyTcEvBinds, sc_lam_args) }
910
911
912
913
  where
    n_silent     = dfunNSilent dfun_id
    orig_ev_vars = drop n_silent dfun_ev_vars

914
915
    sc_lam_args = map (find dfun_ev_vars) sc_theta
    find [] pred 
916
      = pprPanic "tcInstDecl2" (ppr dfun_id $$ ppr (idType dfun_id) $$ ppr pred)
917
918
919
    find (ev:evs) pred 
      | pred `eqPred` evVarPred ev = ev
      | otherwise                  = find evs pred
920
921

----------------------
922
923
924
mkMethIds :: HsSigFun -> Class -> [TcTyVar] -> [EvVar] 
          -> [TcType] -> Id -> TcM (TcId, TcSigInfo)
mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
925
926
927
  = do  { let sel_occ = nameOccName sel_name
        ; meth_name <- newName (mkClassOpAuxOcc sel_occ)
        ; local_meth_name <- newName sel_occ
Gabor Greif's avatar
typos    
Gabor Greif committed
928
                  -- Base the local_meth_name on the selector name, because
929
930
931
932
933
934
935
936
                  -- type errors from tcInstanceMethodBody come from here

        ; local_meth_sig <- case lookupHsSig sig_fn sel_name of
            Just hs_ty  -- There is a signature in the instance declaration
               -> do { sig_ty <- check_inst_sig hs_ty
                     ; instTcTySig hs_ty sig_ty local_meth_name }

            Nothing     -- No type signature
937
938
               -> do { loc <- getSrcSpanM
                     ; instTcTySigFromId loc (mkLocalId local_meth_name local_meth_ty) }
939
940
941
942
943
944
945
946
947
              -- Absent a type sig, there are no new scoped type variables here
              -- Only the ones from the instance decl itself, which are already
              -- in scope.  Example:
              --      class C a where { op :: forall b. Eq b => ... }
              --      instance C [c] where { op = <rhs> }
              -- In <rhs>, 'c' is scope but 'b' is not!

        ; let meth_id = mkLocalId meth_name meth_ty
        ; return (meth_id, local_meth_sig) }
948
  where
949
950
951
952
953
954
955
956
957
958
    sel_name      = idName sel_id
    local_meth_ty = instantiateMethod clas sel_id inst_tys
    meth_ty       = mkForAllTys tyvars $ mkPiTypes dfun_ev_vars local_meth_ty

    -- Check that any type signatures have exactly the right type
    check_inst_sig hs_ty@(L loc _) 
       = setSrcSpan loc $ 
         do { sig_ty <- tcHsSigType (FunSigCtxt sel_name) hs_ty
            ; inst_sigs <- xoptM Opt_InstanceSigs
            ; if inst_sigs then 
959
960
                unless (sig_ty `eqType` local_meth_ty)
                       (badInstSigErr sel_name local_meth_ty)
961
962
963
              else
                addErrTc (misplacedInstSig sel_name hs_ty)
            ; return sig_ty }
964

965
badInstSigErr :: Name -> Type -> TcM ()
966
badInstSigErr meth ty
967
968
969
970
971
972
973
974
975
976
  = do { env0 <- tcInitTidyEnv
       ; let tidy_ty = tidyType env0 ty
                 -- Tidy the type using the ambient TidyEnv, 
                 -- to avoid apparent name capture (Trac #7475)
                 --    class C a where { op :: a -> b }
                 --    instance C (a->b) where
                 --       op :: forall x. x
                 --       op = ...blah...
       ; addErrTc (hang (ptext (sLit "Method signature does not match class; it should be"))
                      2 (pprPrefixName meth <+> dcolon <+> ppr tidy_ty)) }
977

978
979
misplacedInstSig :: Name -> LHsType Name -> SDoc
misplacedInstSig name hs_ty
980
  = vcat [ hang (ptext (sLit "Illegal type signature in instance declaration:"))
981
              2 (hang (pprPrefixName name)
982
983
984
                    2 (dcolon <+> ppr hs_ty))
         , ptext (sLit "(Use -XInstanceSigs to allow this)") ]

985
------------------------------
986
tcSpecInstPrags :: DFunId -> InstBindings Name
987
988
989
990
991
992
                -> TcM ([Located TcSpecPrag], PragFun)
tcSpecInstPrags _ (NewTypeDerived {})
  = return ([], \_ -> [])
tcSpecInstPrags dfun_id (VanillaInst binds uprags _)
  = do { spec_inst_prags <- mapM (wrapLocM (tcSpecInst dfun_id)) $
                            filter isSpecInstLSig uprags
dterei's avatar
dterei committed
993
             -- The filter removes the pragmas for methods
994
       ; return (spec_inst_prags, mkPragFun uprags binds) }
995
\end{code}
996

997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
Note [Silent superclass arguments]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See Trac #3731, #4809, #5751, #5913, #6117, which all
describe somewhat more complicated situations, but ones
encountered in practice.  

      THE PROBLEM

The problem is that it is all too easy to create a class whose
superclass is bottom when it should not be.

1008
1009
1010
1011
Consider the following (extreme) situation:
        class C a => D a where ...
        instance D [a] => D [a] where ...
Although this looks wrong (assume D [a] to prove D [a]), it is only a
1012
1013
1014
more extreme case of what happens with recursive dictionaries, and it
can, just about, make sense because the methods do some work before
recursing.
1015

1016
To implement the dfun we must generate code for the superclass C [a],
1017
1018
which we had better not get by superclass selection from the supplied
argument:
1019
1020
       dfun :: forall a. D [a] -> D [a]
       dfun = \d::D [a] -> MkD (scsel d) ..
1021

1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
Otherwise if we later encounter a situation where
we have a [Wanted] dw::D [a] we might solve it thus:
     dw := dfun dw
Which is all fine except that now ** the superclass C is bottom **!

      THE SOLUTION

Our solution to this problem "silent superclass arguments".  We pass
to each dfun some ``silent superclass arguments’’, which are the
immediate superclasses of the dictionary we are trying to
construct. In our example:
       dfun :: forall a. C [a] -> D [a] -> D [a]
       dfun = \(dc::C [a]) (dd::D [a]) -> DOrd dc ...
1035
Notice the extra (dc :: C [a]) argument compared to the previous version.
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054

This gives us:

     -----------------------------------------------------------
     DFun Superclass Invariant
     ~~~~~~~~~~~~~~~~~~~~~~~~
     In the body of a DFun, every superclass argument to the
     returned dictionary is
       either   * one of the arguments of the DFun,
       or       * constant, bound at top level
     -----------------------------------------------------------

This net effect is that it is safe to treat a dfun application as
wrapping a dictionary constructor around its arguments (in particular,
a dfun never picks superclasses from the arguments under the
dictionary constructor). No superclass is hidden inside a dfun
application.

The extra arguments required to satisfy the DFun Superclass Invariant
1055
1056
1057
1058
1059
1060
1061
always come first, and are called the "silent" arguments.  You can
find out how many silent arguments there are using Id.dfunNSilent;
and then you can just drop that number of arguments to see the ones
that were in the original instance declaration.

DFun types are built (only) by MkId.mkDictFunId, so that is where we
decide what silent arguments are to be added.
1062
1063
1064
1065
1066
1067
1068
1069
1070

In our example, if we had  [Wanted] dw :: D [a] we would get via the instance:
    dw := dfun d1 d2
    [Wanted] (d1 :: C [a])
    [Wanted] (d2 :: D [a])

And now, though we *can* solve: 
     d2 := dw
That's fine; and we solve d1:C[a] separately.
1071

dterei's avatar
dterei committed
1072
1073
Test case SCLoop tests this fix.

1074
1075
1076
1077
1078
1079
1080
1081
Note [SPECIALISE instance pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

   instance (Ix a, Ix b) => Ix (a,b) where
     {-# SPECIALISE instance Ix (Int,Int) #-}
     range (x,y) = ...

1082
1083
1084
We make a specialised version of the dictionary function, AND
specialised versions of each *method*.  Thus we should generate
something like this:
1085

1086
  $dfIxPair :: (Ix a, Ix b) => Ix (a,b)