TcInstDcls.lhs 58.9 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 23 24 25 26 27
import TcTyClsDecls( tcAddImplicits, tcAddFamInstCtxt, tcSynFamInstDecl, 
                     wrongKindOfFamily, tcFamTyPats, kcTyDefn, dataDeclChecks,
                     tcConDecls, checkValidTyCon, badATErr, wrongATArgErr )
import TcClassDcl( tcClassDecl2, 
                   HsSigFun, lookupHsSig, mkHsSigFun, emptyHsSigs,
                   findMethodBind, instantiateMethod, tcInstanceMethodBody )
dterei's avatar
dterei committed
28
import TcPat      ( addInlinePrags )
Ian Lynagh's avatar
Ian Lynagh committed
29
import TcRnMonad
30 31
import TcMType
import TcType
32
import BuildTyCl
33 34 35 36 37 38 39 40
import Inst
import InstEnv
import FamInst
import FamInstEnv
import TcDeriv
import TcEnv
import TcHsType
import TcUnify
dterei's avatar
dterei committed
41
import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
42
import CoreSyn    ( DFunArg(..) )
43
import Type
44
import TcEvidence
45 46 47 48
import TyCon
import DataCon
import Class
import Var
49
import VarEnv
50
import VarSet     ( mkVarSet, subVarSet, varSetElems )
51
import Pair
52
import CoreUnfold ( mkDFunUnfolding )
53
import CoreSyn    ( Expr(Var), CoreExpr )
54
import PrelNames  ( typeableClassNames )
dterei's avatar
dterei committed
55 56 57 58

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

69
import Control.Monad
dterei's avatar
dterei committed
70
import Maybes     ( orElse )
71 72 73
\end{code}

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

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.

83 84 85 86 87 88

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

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

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

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

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

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

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

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

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

 * 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
185
   a suitable constructor application -- inlining df "on the fly" as it
186 187 188 189 190 191 192 193 194 195 196 197
   were.

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

 * We make 'df' CONLIKE, so that shared uses stil match; eg
      let d = df d1 d2
      in ...(op2 d)...(op1 d)...

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

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

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

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

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

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

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

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

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

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

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

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
wasn't due to the indirction).
241

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

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

262 263
    class DeepSeq a where
      deepSeq :: a -> b -> b
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 290 291
    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
292

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

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

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

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

334

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

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

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

353

354 355

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

Gather up the instance declarations from their various sources

363
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
364 365 366 367 368
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
369
           [InstInfo Name],     -- Source-code instance decls to process;
Ian Lynagh's avatar
Ian Lynagh committed
370 371
                                -- contains all dfuns for this module
           HsValBinds Name)     -- Supporting bindings for derived instances
372

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

379
            -- Do class and family instance declarations
380 381 382 383 384 385
       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
       ; let (local_infos_s, fam_insts_s) = unzip stuff
             local_infos = concat local_infos_s
             fam_insts   = concat fam_insts_s
       ; addClsInsts local_infos $
         addFamInsts fam_insts   $ 
386

387
    do {    -- Compute instances from "deriving" clauses;
388 389 390 391
            -- 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
392
         failIfErrsM    -- If the addInsts stuff gave any errors, don't
dterei's avatar
dterei committed
393 394
                        -- try the deriving stuff, because that may give
                        -- more errors still
dreixel's avatar
dreixel committed
395

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

404

405 406
       -- Check that if the module is compiled with -XSafe, there are no
       -- hand written instances of Typeable as then unsafe casts could be
dreixel's avatar
dreixel committed
407
       -- performed. Derived instances are OK.
408
       ; dflags <- getDynFlags
409
       ; when (safeLanguageOn dflags) $
410
             mapM_ (\x -> when (typInstCheck x)
411
                               (addErrAt (getSrcSpan $ iSpec x) typInstErr))
412
                   local_infos
413 414
       -- As above but for Safe Inference mode.
       ; when (safeInferOn dflags) $
415
             mapM_ (\x -> when (typInstCheck x) recordUnsafeInfer) local_infos
416

dreixel's avatar
dreixel committed
417
       ; return ( gbl_env
418
                , bagToList deriv_inst_info ++ local_infos
419
                , deriv_binds)
420
    }}
dterei's avatar
dterei committed
421
  where
422
    typInstCheck ty = is_cls (iSpec ty) `elem` typeableClassNames
dterei's avatar
dterei committed
423 424
    typInstErr = ptext $ sLit $ "Can't create hand written instances of Typeable in Safe"
                              ++ " Haskell! Can only derive them"
425

426 427
addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
addClsInsts infos thing_inside
428
  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
429

430 431 432 433 434
addFamInsts :: [FamInst] -> TcM a -> TcM a
-- Extend (a) the family instance envt
--        (b) the type envt with stuff from data type decls
addFamInsts fam_insts thing_inside
  = tcExtendLocalFamInstEnv fam_insts $ 
435
    tcExtendGlobalEnv things $
436 437
    do { traceTc "addFamInsts" (pprFamInsts fam_insts)
       ; tcg_env <- tcAddImplicits things
438 439 440 441 442
       ; setGblEnv tcg_env thing_inside }
  where
    axioms = map famInstAxiom fam_insts
    tycons = famInstsRepTyCons fam_insts
    things = map ATyCon tycons ++ map ACoAxiom axioms 
SamB's avatar
SamB committed
443
\end{code}
444

445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
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.


462
\begin{code}
463 464
tcLocalInstDecl :: LInstDecl Name
                -> TcM ([InstInfo Name], [FamInst])
Ian Lynagh's avatar
Ian Lynagh committed
465 466 467 468
        -- A source-file instance declaration
        -- Type-check all the stuff before the "where"
        --
        -- We check for respectable instance type, and context
469
tcLocalInstDecl (L loc (FamInstD { lid_inst = decl }))
470
  = setSrcSpan loc      $
471
    tcAddFamInstCtxt decl  $
472 473 474
    do { fam_inst <- tcFamInstDecl TopLevel decl
       ; return ([], [fam_inst]) }

475 476
tcLocalInstDecl (L loc (ClsInstD { cid_poly_ty = poly_ty, cid_binds = binds
                                 , cid_sigs = uprags, cid_fam_insts = ats }))
dterei's avatar
dterei committed
477
  = setSrcSpan loc                      $
Ian Lynagh's avatar
Ian Lynagh committed
478 479 480 481 482 483
    addErrCtxt (instDeclCtxt1 poly_ty)  $

    do  { is_boot <- tcIsHsBoot
        ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
                  badBootDeclErr

dreixel's avatar
dreixel committed
484
        ; (tyvars, theta, clas, inst_tys) <- tcHsInstHead InstDeclCtxt poly_ty
485 486 487
        ; let mini_env   = mkVarEnv (classTyVars clas `zip` inst_tys)
              mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env
                           
488
        -- Next, process any associated types.
489
        ; traceTc "tcLocalInstDecl" (ppr poly_ty)
490 491
        ; fam_insts0 <- tcExtendTyVarEnv tyvars $
                        mapAndRecoverM (tcAssocDecl clas mini_env) ats
492

dreixel's avatar
dreixel committed
493
        -- Check for missing associated types and build them
494
        -- from their defaults (if available)
495
        ; let defined_ats = mkNameSet $ map famInstDeclName ats
496

497
              mk_deflt_at_instances :: ClassATItem -> TcM [FamInst]
498
              mk_deflt_at_instances (fam_tc, defs)
499
                 -- User supplied instances ==> everything is OK
500 501 502
                | tyConName fam_tc `elemNameSet` defined_ats 
                = return []

503
                 -- No defaults ==> generate a warning
504 505 506 507
                | null defs
                = do { warnMissingMethodOrAT "associated type" (tyConName fam_tc)
                     ; return [] }

508
                 -- No user instance, have defaults ==> instatiate them
509 510 511 512 513 514 515 516 517 518 519
                 -- 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 
                = forM defs $ \(ATD _tvs pat_tys rhs _loc) ->
                  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'
                     ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
520
                       return (mkSynFamInst rep_tc_name tvs' fam_tc pat_tys' rhs') }
521

522
        ; fam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
523
        
Ian Lynagh's avatar
Ian Lynagh committed
524 525
        -- Finally, construct the Core representation of the instance.
        -- (This no longer includes the associated types.)
526
        ; dfun_name <- newDFunName clas inst_tys (getLoc poly_ty)
dterei's avatar
dterei committed
527
                -- Dfun location is that of instance *header*
528

Ian Lynagh's avatar
Ian Lynagh committed
529
        ; overlap_flag <- getOverlapFlag
530 531 532 533
        ; let dfun  	= mkDictFunId dfun_name tyvars theta clas inst_tys
              ispec 	= mkLocalInstance dfun overlap_flag
              inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }

534
        ; return ( [inst_info], fam_insts0 ++ concat fam_insts1) }
535 536
\end{code}

537 538 539 540 541 542 543 544 545 546 547 548
%************************************************************************
%*                                                                      *
               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}
549
tcFamInstDecl :: TopLevelFlag -> FamInstDecl Name -> TcM FamInst
550
tcFamInstDecl top_lvl decl
551
  = do { -- Type family instances require -XTypeFamilies
552
         -- and can't (currently) be in an hs-boot file
dreixel's avatar
dreixel committed
553
       ; traceTc "tcFamInstDecl" (ppr decl)
554
       ; let fam_tc_lname = fid_tycon decl
555 556 557 558 559 560 561 562 563 564 565 566 567 568
       ; 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
       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
       ; when (isTopLevel top_lvl && isTyConAssoc fam_tc)
              (addErr $ assocInClassErr fam_tc_lname)

         -- Now check the type/data instance itself
         -- This is where type and data decls are treated separately
569
       ; tcFamInstDecl1 fam_tc decl }
570

571
tcFamInstDecl1 :: TyCon -> FamInstDecl Name -> TcM FamInst
572 573

  -- "type instance"
574 575
tcFamInstDecl1 fam_tc decl@(FamInstDecl { fid_tycon = fam_tc_name
                                        , fid_defn = TySynonym {} })
dreixel's avatar
dreixel committed
576 577
  = do { -- (1) do the work of verifying the synonym
       ; (t_tvs, t_typats, t_rhs) <- tcSynFamInstDecl fam_tc decl
578 579 580 581 582

         -- (2) check the well-formedness of the instance
       ; checkValidFamInst t_typats t_rhs

         -- (3) construct representation tycon
583
       ; rep_tc_name <- newFamInstAxiomName fam_tc_name t_typats
584 585

       ; return (mkSynFamInst rep_tc_name t_tvs fam_tc t_typats t_rhs) }
586 587

  -- "newtype instance" and "data instance"
588 589 590 591 592
tcFamInstDecl1 fam_tc 
    (FamInstDecl { fid_pats = pats
                 , fid_tycon = fam_tc_name
                 , fid_defn = defn@TyData { td_ND = new_or_data, td_cType = cType
                                          , td_ctxt = ctxt, td_cons = cons } })
dreixel's avatar
dreixel committed
593
  = do { -- Check that the family declaration is for the right kind
594 595 596
         checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
       ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)

dreixel's avatar
dreixel committed
597
         -- Kind check type patterns
598
       ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ 
599
           \tvs' pats' res_kind -> do
600

dreixel's avatar
dreixel committed
601 602 603 604 605 606
         -- Check that left-hand side contains no type family applications
         -- (vanilla synonyms are fine, though, and we checked for
         -- foralls earlier)
       { mapM_ checkTyFamFreeness pats'
         
         -- Result kind must be '*' (otherwise, we have too few patterns)
607
       ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
608

609
       ; stupid_theta <- tcHsContext ctxt
610
       ; dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
611

dreixel's avatar
dreixel committed
612
         -- Construct representation tycon
613
       ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
614
       ; axiom_name  <- newImplicitBinder rep_tc_name mkInstTyCoOcc
615
       ; let ex_ok = True       -- Existentials ok for type families!
616 617 618 619
             orig_res_ty = mkTyConApp fam_tc pats'

       ; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
           do { data_cons <- tcConDecls new_or_data ex_ok rec_rep_tc
dreixel's avatar
dreixel committed
620
                                       (tvs', orig_res_ty) cons
621 622 623 624 625 626
              ; 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)
              ; let fam_inst = mkDataFamInst axiom_name tvs' fam_tc pats' rep_tc
                    parent   = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats'
627
                    rep_tc   = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs 
628
                                             Recursive h98_syntax parent
629 630 631 632 633
                 -- 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.
634 635 636 637 638
              ; return (rep_tc, fam_inst) }

         -- Remember to check validity; no recursion to worry about here
       ; checkValidTyCon rep_tc
       ; return fam_inst } }
dreixel's avatar
dreixel committed
639
    where
640
       h98_syntax = case cons of      -- All constructors have same shape
641 642 643 644 645
                        L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
                        _ -> True


----------------
646 647 648
tcAssocDecl :: Class              -- ^ Class of associated type
            -> VarEnv Type        -- ^ Instantiation of class TyVars
            -> LFamInstDecl Name  -- ^ RHS
649
            -> TcM FamInst
650 651
tcAssocDecl clas mini_env (L loc decl)
  = setSrcSpan loc      $
652
    tcAddFamInstCtxt decl  $
653 654 655
    do { fam_inst <- tcFamInstDecl NotTopLevel decl
       ; let (fam_tc, at_tys) = famInstLHS fam_inst

656 657
       -- Check that the associated type comes from this class
       ; checkTc (Just clas == tyConAssoc_maybe fam_tc)
658
                 (badATErr (className clas) (tyConName fam_tc))
659

dreixel's avatar
dreixel committed
660
       -- See Note [Checking consistent instantiation] in TcTyClsDecls
661 662
       ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys

663
       ; return fam_inst }
664 665 666 667 668
  where
    check_arg fam_tc_tv at_ty
      | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
      = checkTc (inst_ty `eqType` at_ty) 
                (wrongATArgErr at_ty inst_ty)
669 670
                -- No need to instantiate here, becuase the axiom
                -- uses the same type variables as the assocated class
671 672 673 674 675 676
      | otherwise
      = return ()   -- Allow non-type-variable instantiation
                    -- See Note [Associated type instances]
\end{code}


677
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
678
%*                                                                      *
679
      Type-checking instance declarations, pass 2
Ian Lynagh's avatar
Ian Lynagh committed
680
%*                                                                      *
681 682 683
%************************************************************************

\begin{code}
684
tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
685
             -> TcM (LHsBinds Id)
Ian Lynagh's avatar
Ian Lynagh committed
686 687
-- (a) From each class declaration,
--      generate any default-method bindings
688
-- (b) From each instance decl
Ian Lynagh's avatar
Ian Lynagh committed
689
--      generate the dfun binding
690 691

tcInstDecls2 tycl_decls inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
692
  = do  { -- (a) Default methods from class decls
693
          let class_decls = filter (isClassDecl . unLoc) tycl_decls
694
        ; dm_binds_s <- mapM tcClassDecl2 class_decls
695
        ; let dm_binds = unionManyBags dm_binds_s
dterei's avatar
dterei committed
696

Ian Lynagh's avatar
Ian Lynagh committed
697
          -- (b) instance declarations
dterei's avatar
dterei committed
698 699 700
        ; let dm_ids = collectHsBindsBinders dm_binds
              -- Add the default method Ids (again)
              -- See Note [Default methods and instances]
701
        ; inst_binds_s <- tcExtendLetEnv TopLevel dm_ids $
702
                          mapM tcInstDecl2 inst_decls
Ian Lynagh's avatar
Ian Lynagh committed
703 704

          -- Done
705
        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
706 707
\end{code}

708 709 710 711 712 713 714 715 716 717
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).

718
So right here in tcInstDecls2 we must re-extend the type envt with
719
the default method Ids replete with their INLINE pragmas.  Urk.
720

721
\begin{code}
722 723 724 725 726 727

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
728
    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
729
    do {  -- Instantiate the instance decl with skolem constants
730
       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id)
dimitris's avatar
dimitris committed
731 732 733
                     -- We instantiate the dfun_id with superSkolems.
                     -- See Note [Subtle interaction of recursion and overlap]
                     -- and Note [Binding when looking up instances]
734
       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
735
             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
736
             sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta
737

738
       ; dfun_ev_vars <- newEvVars dfun_theta
739

740 741
       ; (sc_binds, sc_ev_vars, sc_dfun_args) 
            <- tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta'
742 743 744

       -- Deal with 'SPECIALISE instance' pragmas
       -- See Note [SPECIALISE instance pragmas]
745
       ; spec_inst_info <- tcSpecInstPrags dfun_id ibinds
746 747

        -- Typecheck the methods
dterei's avatar
dterei committed
748
       ; (meth_ids, meth_binds)
749 750 751 752 753
           <- 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
754
                                inst_tys spec_inst_info
755
                                op_items ibinds
756

757
       -- Create the result bindings
batterseapower's avatar
batterseapower committed
758
       ; self_dict <- newDict clas inst_tys
759 760
       ; let class_tc      = classTyCon clas
             [dict_constr] = tyConDataCons class_tc
Simon Peyton Jones's avatar
Simon Peyton Jones committed
761 762
             dict_bind     = mkVarBind self_dict (L loc con_app_args)

763 764 765 766
                     -- 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
767
                     -- member) are dealt with by the common MkId.mkDataConWrapId
dterei's avatar
dterei committed
768 769 770 771
                     -- 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
772 773
             con_app_tys  = wrapId (mkWpTyApps inst_tys)
                                   (dataConWrapId dict_constr)
774
             con_app_scs  = mkHsWrap (mkWpEvApps (map EvId sc_ev_vars)) con_app_tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
775 776 777 778 779 780
             con_app_args = foldl mk_app con_app_scs $
                            map (wrapId arg_wrapper) meth_ids

             mk_app :: HsExpr Id -> HsExpr Id -> HsExpr Id
             mk_app fun arg = HsApp (L loc fun) (L loc arg)

781
             inst_tv_tys = mkTyVarTys inst_tyvars
Simon Peyton Jones's avatar
Simon Peyton Jones committed
782
             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
783

dterei's avatar
dterei committed
784 785 786
                -- Do not inline the dfun; instead give it a magic DFunFunfolding
                -- See Note [ClassOp/DFun selection]
                -- See also note [Single-method classes]
787 788 789 790
             dfun_id_w_fun
                | isNewTyCon class_tc
                = dfun_id `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
                | otherwise
Simon Peyton Jones's avatar
Simon Peyton Jones committed
791
                = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_ty dfun_args
792
                          `setInlinePragma` dfunInlinePragma
Simon Peyton Jones's avatar
Simon Peyton Jones committed
793

794 795
             dfun_args :: [DFunArg CoreExpr]
             dfun_args = sc_dfun_args ++ map (DFunPolyArg . Var) meth_ids
796

797
             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id_w_fun
798 799
                          , abe_mono = self_dict, abe_prags = noSpecPrags }
                          -- NB: noSpecPrags, see Note [SPECIALISE instance pragmas]
800
             main_bind = AbsBinds { abs_tvs = inst_tyvars
801
                                  , abs_ev_vars = dfun_ev_vars
802
                                  , abs_exports = [export]
803
                                  , abs_ev_binds = sc_binds
804
                                  , abs_binds = unitBag dict_bind }
805

806
       ; return (unitBag (L loc main_bind) `unionBags`
807
                 listToBag meth_binds)
808
       }
809 810 811 812 813
 where
   dfun_ty   = idType dfun_id
   dfun_id   = instanceDFunId ispec
   loc       = getSrcSpan dfun_id

814
------------------------------
815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839
tcSuperClasses :: DFunId -> [TcTyVar] -> [EvVar] -> TcThetaType
               -> TcM (TcEvBinds, [EvVar], [DFunArg CoreExpr])
-- 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 
         then return (sc_binds,       sc_evs,      map (DFunPolyArg . Var) sc_evs)
         else return (emptyTcEvBinds, sc_lam_args, sc_dfun_args) }
  where
    n_silent     = dfunNSilent dfun_id
    n_tv_args    = length inst_tyvars
    orig_ev_vars = drop n_silent dfun_ev_vars

    (sc_lam_args, sc_dfun_args) = unzip (map (find n_tv_args dfun_ev_vars) sc_theta)
    find _ [] pred 
      = pprPanic "tcInstDecl2" (ppr dfun_id $$ ppr (idType dfun_id) $$ ppr pred)
    find i (ev:evs) pred 
      | pred `eqPred` evVarPred ev = (ev, DFunLamArg i)
      | otherwise                  = find (i+1) evs pred

----------------------
840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865
mkMethIds :: HsSigFun -> Class -> [TcTyVar] -> [EvVar] 
          -> [TcType] -> Id -> TcM (TcId, TcSigInfo)
mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
  = do  { uniq <- newUnique
        ; loc <- getSrcSpanM
        ; let meth_name = mkDerivedInternalName mkClassOpAuxOcc uniq sel_name
        ; local_meth_name <- newLocalName sel_name
                  -- Base the local_meth_name on the selector name, becuase
                  -- 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
               -> instTcTySigFromId loc (mkLocalId local_meth_name local_meth_ty)
              -- 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) }
866
  where
867 868 869 870 871 872 873 874 875 876
    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 
877 878
                unless (sig_ty `eqType` local_meth_ty)
                       (badInstSigErr sel_name local_meth_ty)
879 880 881
              else
                addErrTc (misplacedInstSig sel_name hs_ty)
            ; return sig_ty }
882

883
badInstSigErr :: Name -> Type -> TcM ()
884
badInstSigErr meth ty
885 886 887 888 889 890 891 892 893 894
  = 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)) }
895

896 897
misplacedInstSig :: Name -> LHsType Name -> SDoc
misplacedInstSig name hs_ty
898
  = vcat [ hang (ptext (sLit "Illegal type signature in instance declaration:"))
899
              2 (hang (pprPrefixName name)
900 901 902
                    2 (dcolon <+> ppr hs_ty))
         , ptext (sLit "(Use -XInstanceSigs to allow this)") ]

903
------------------------------
904
tcSpecInstPrags :: DFunId -> InstBindings Name
905 906 907 908 909 910
                -> 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
911
             -- The filter removes the pragmas for methods
912
       ; return (spec_inst_prags, mkPragFun uprags binds) }
913
\end{code}
914

915 916 917 918 919 920 921 922 923 924 925
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.

926 927 928 929
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
930 931 932
more extreme case of what happens with recursive dictionaries, and it
can, just about, make sense because the methods do some work before
recursing.
933

934
To implement the dfun we must generate code for the superclass C [a],
935 936
which we had better not get by superclass selection from the supplied
argument:
937 938
       dfun :: forall a. D [a] -> D [a]
       dfun = \d::D [a] -> MkD (scsel d) ..
939

940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984
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 ...
Notice teh extra (dc :: C [a]) argument compared to the previous version.

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
always come first, and are called the "silent" arguments.  DFun types
are built (only) by MkId.mkDictFunId, so that is where we decide
what silent arguments are to be added.

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

dterei's avatar
dterei committed
986