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

Type subsumption and unification
7
8
9

\begin{code}
module TcUnify (
Ian Lynagh's avatar
Ian Lynagh committed
10
11
12
        -- Full-blown subsumption
  tcSubExp, tcGen,
  checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
13

Ian Lynagh's avatar
Ian Lynagh committed
14
        -- Various unifications
15
  unifyType, unifyTypeList, unifyTheta,
Ian Lynagh's avatar
Ian Lynagh committed
16
17
18
  unifyKind, unifyKinds, unifyFunKind,
  checkExpectedKind,
  preSubType, boxyMatchTypes,
19
20
21

  --------------------------------
  -- Holes
Ian Lynagh's avatar
Ian Lynagh committed
22
  tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
23
  boxyUnify, boxyUnifyList, zapToMonotype,
24
  boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy,
25
  wrapFunResCoercion
26
27
28
29
  ) where

#include "HsVersions.h"

30
31
32
33
34
35
import HsSyn
import TypeRep

import TcMType
import TcSimplify
import TcEnv
36
import TcTyFuns
37
import TcIface
38
import TcRnMonad         -- TcType, amongst others
39
40
import TcType
import Type
41
import Coercion
42
43
44
45
46
import TysPrim
import Inst
import TyCon
import TysWiredIn
import Var
47
import VarSet
48
import VarEnv
49
50
51
52
53
import Name
import ErrUtils
import Maybes
import BasicTypes
import Util
54
import Outputable
55
import FastString
56
57

import Control.Monad
58
\end{code}
59

60
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
61
%*                                                                      *
62
\subsection{'hole' type variables}
Ian Lynagh's avatar
Ian Lynagh committed
63
%*                                                                      *
64
65
66
%************************************************************************

\begin{code}
67
tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
68
tcInfer tc_infer = withBox openTypeKind tc_infer
69
\end{code}
70
71
72


%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
73
74
75
%*                                                                      *
        subFunTys
%*                                                                      *
76
77
78
%************************************************************************

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
79
subFunTys :: SDoc  -- Something like "The function f has 3 arguments"
Ian Lynagh's avatar
Ian Lynagh committed
80
81
82
83
84
                   -- or "The abstraction (\x.e) takes 1 argument"
          -> Arity              -- Expected # of args
          -> BoxyRhoType        -- res_ty
          -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
          -> TcM (HsWrapper, a)
85
86
-- Attempt to decompse res_ty to have enough top-level arrows to
-- match the number of patterns in the match group
Ian Lynagh's avatar
Ian Lynagh committed
87
--
88
89
-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
-- and the inner call to thing_inside passes args: [a1,...,an], b
90
-- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty
91
--
92
-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
93

94

Ian Lynagh's avatar
Ian Lynagh committed
95
{-      Error messages from subFunTys
96
97
98
99
100
101
102
103
104
105
106
107
108
109

   The abstraction `\Just 1 -> ...' has two arguments
   but its type `Maybe a -> a' has only one

   The equation(s) for `f' have two arguments
   but its type `Maybe a -> a' has only one

   The section `(f 3)' requires 'f' to take two arguments
   but its type `Int -> Int' has only one

   The function 'f' is applied to two arguments
   but its type `Int -> Int' has only one
-}

110
111
112

subFunTys error_herald n_pats res_ty thing_inside
  = loop n_pats [] res_ty
113
  where
Ian Lynagh's avatar
Ian Lynagh committed
114
115
116
        -- In 'loop', the parameter 'arg_tys' accumulates
        -- the arg types so far, in *reverse order*
        -- INVARIANT:   res_ty :: *
117
    loop n args_so_far res_ty
Ian Lynagh's avatar
Ian Lynagh committed
118
        | Just res_ty' <- tcView res_ty  = loop n args_so_far res_ty'
119
120

    loop n args_so_far res_ty
Ian Lynagh's avatar
Ian Lynagh committed
121
122
        | isSigmaTy res_ty      -- Do this before checking n==0, because we
                                -- guarantee to return a BoxyRhoType, not a
123
                                -- BoxySigmaType
Ian Lynagh's avatar
Ian Lynagh committed
124
125
126
        = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
                                         loop n args_so_far res_ty'
             ; return (gen_fn <.> co_fn, res) }
127

Ian Lynagh's avatar
Ian Lynagh committed
128
129
130
    loop 0 args_so_far res_ty
        = do { res <- thing_inside (reverse args_so_far) res_ty
             ; return (idHsWrapper, res) }
131

Ian Lynagh's avatar
Ian Lynagh committed
132
133
134
135
    loop n args_so_far (FunTy arg_ty res_ty)
        = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
             ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
             ; return (co_fn', res) }
136

137
        -- Try to normalise synonym families and defer if that's not possible
Ian Lynagh's avatar
Ian Lynagh committed
138
    loop n args_so_far ty@(TyConApp tc _)
139
140
141
        | isOpenSynTyCon tc
        = do { (coi1, ty') <- tcNormaliseFamInst ty
             ; case coi1 of
Ian Lynagh's avatar
Ian Lynagh committed
142
                 IdCo   -> defer n args_so_far ty
143
                                    -- no progress, but maybe solvable => defer
144
                 ACo _  ->          -- progress: so lets try again
Ian Lynagh's avatar
Ian Lynagh committed
145
146
147
                   do { (co_fn, res) <- loop n args_so_far ty'
                      ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res)
                      }
148
149
             }

Ian Lynagh's avatar
Ian Lynagh committed
150
151
152
153
        -- res_ty might have a type variable at the head, such as (a b c),
        -- in which case we must fill in with (->).  Simplest thing to do
        -- is to use boxyUnify, but we catch failure and generate our own
        -- error message on failure
154
    loop n args_so_far res_ty@(AppTy _ _)
Ian Lynagh's avatar
Ian Lynagh committed
155
156
        = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind]
             ; (_, mb_coi) <- tryTcErrs $
157
                                boxyUnify res_ty (FunTy arg_ty' res_ty')
Ian Lynagh's avatar
Ian Lynagh committed
158
159
160
             ; if isNothing mb_coi then bale_out args_so_far
               else do { let coi = expectJust "subFunTys" mb_coi
                       ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty'
161
162
                                                                   res_ty')
                       ; return (co_fn <.> coiToHsWrapper coi, res)
Ian Lynagh's avatar
Ian Lynagh committed
163
164
                       }
             }
165

166
    loop n args_so_far ty@(TyVarTy tv)
167
        | isTyConableTyVar tv
Ian Lynagh's avatar
Ian Lynagh committed
168
169
170
171
        = do { cts <- readMetaTyVar tv
             ; case cts of
                 Indirect ty -> loop n args_so_far ty
                 Flexi ->
172
                   do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
Ian Lynagh's avatar
Ian Lynagh committed
173
                      ; res <- thing_inside (reverse args_so_far ++ arg_tys)
174
                                            res_ty
Ian Lynagh's avatar
Ian Lynagh committed
175
                      ; return (idHsWrapper, res) } }
176
        | otherwise             -- defer as tyvar may be refined by equalities
177
        = defer n args_so_far ty
Ian Lynagh's avatar
Ian Lynagh committed
178
179
180
181
182
183
        where
          mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
          mk_res_ty [] = panic "TcUnify.mk_res_ty1"
          kinds = openTypeKind : take n (repeat argTypeKind)
                -- Note argTypeKind: the args can have an unboxed type,
                -- but not an unboxed tuple.
184

Ian Lynagh's avatar
Ian Lynagh committed
185
    loop _ args_so_far _ = bale_out args_so_far
186

187
         -- Build a template type a1 -> ... -> an -> b and defer an equality
188
189
         -- between that template and the expected result type res_ty; then,
         -- use the template to type the thing_inside
190
191
    defer n args_so_far ty
      = do { arg_tys <- newFlexiTyVarTys n argTypeKind
192
193
           ; res_ty' <- newFlexiTyVarTy openTypeKind
           ; let fun_ty = mkFunTys arg_tys res_ty'
194
195
196
                 err    = error_herald <> comma $$
                          text "which does not match its type"
           ; coi <- addErrCtxt err $
197
                    defer_unification (Unify False fun_ty ty) False fun_ty ty
198
           ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
199
200
201
           ; return (coiToHsWrapper coi, res)
           }

Ian Lynagh's avatar
Ian Lynagh committed
202
203
204
205
206
207
208
209
210
211
212
    bale_out args_so_far
        = do { env0 <- tcInitTidyEnv
             ; res_ty' <- zonkTcType res_ty
             ; let (env1, res_ty'') = tidyOpenType env0 res_ty'
             ; failWithTcM (env1, mk_msg res_ty'' (length args_so_far)) }

    mk_msg res_ty n_actual
      = error_herald <> comma $$
        sep [ptext (sLit "but its type") <+> quotes (pprType res_ty),
             if n_actual == 0 then ptext (sLit "has none")
             else ptext (sLit "has only") <+> speakN n_actual]
213
214
215
\end{code}

\begin{code}
216
----------------------
Ian Lynagh's avatar
Ian Lynagh committed
217
218
219
boxySplitTyConApp :: TyCon                      -- T :: k1 -> ... -> kn -> *
                  -> BoxyRhoType                -- Expected type (T a b c)
                  -> TcM ([BoxySigmaType],      -- Element types, a b c
220
                          CoercionI)            -- T a b c ~ orig_ty
221
  -- It's used for wired-in tycons, so we call checkWiredInTyCon
222
  -- Precondition: never called with FunTyCon
223
  -- Precondition: input type :: *
224

225
boxySplitTyConApp tc orig_ty
Ian Lynagh's avatar
Ian Lynagh committed
226
227
  = do  { checkWiredInTyCon tc
        ; loop (tyConArity tc) [] orig_ty }
228
  where
Ian Lynagh's avatar
Ian Lynagh committed
229
    loop n_req args_so_far ty
230
231
      | Just ty' <- tcView ty = loop n_req args_so_far ty'

232
    loop n_req args_so_far ty@(TyConApp tycon args)
233
      | tc == tycon
Ian Lynagh's avatar
Ian Lynagh committed
234
235
      = ASSERT( n_req == length args)   -- ty::*
        return (args ++ args_so_far, IdCo)
236
237
238

      | isOpenSynTyCon tycon        -- try to normalise type family application
      = do { (coi1, ty') <- tcNormaliseFamInst ty
Ian Lynagh's avatar
Ian Lynagh committed
239
           ; traceTc $ text "boxySplitTyConApp:" <+>
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
240
                       ppr ty <+> text "==>" <+> ppr ty'
241
           ; case coi1 of
Ian Lynagh's avatar
Ian Lynagh committed
242
               IdCo   -> defer    -- no progress, but maybe solvable => defer
243
               ACo _  ->          -- progress: so lets try again
Ian Lynagh's avatar
Ian Lynagh committed
244
245
246
                 do { (args, coi2) <- loop n_req args_so_far ty'
                    ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
                    }
247
           }
248
249

    loop n_req args_so_far (AppTy fun arg)
250
      | n_req > 0
251
252
253
      = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun
           ; return (args, mkAppTyCoI fun coi arg IdCo)
           }
254
255

    loop n_req args_so_far (TyVarTy tv)
256
      | isTyConableTyVar tv
257
      , res_kind `isSubKind` tyVarKind tv
258
      = do { cts <- readMetaTyVar tv
Ian Lynagh's avatar
Ian Lynagh committed
259
260
261
262
263
           ; case cts of
               Indirect ty -> loop n_req args_so_far ty
               Flexi       -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
                                 ; return (arg_tys ++ args_so_far, IdCo) }
           }
264
265
      | otherwise             -- defer as tyvar may be refined by equalities
      = defer
266
      where
Ian Lynagh's avatar
Ian Lynagh committed
267
        (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
268

269
270
271
272
273
274
275
276
277
278
    loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc)))
                                  orig_ty

    -- defer splitting by generating an equality constraint
    defer = boxySplitDefer arg_kinds mk_res_ty orig_ty
      where
        (arg_kinds, _) = splitKindFunTys (tyConKind tc)

    -- apply splitted tycon to arguments
    mk_res_ty = mkTyConApp tc
279

280
----------------------
281
282
boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
-- Special case for lists
Ian Lynagh's avatar
Ian Lynagh committed
283
boxySplitListTy exp_ty
284
285
 = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty
      ; return (elt_ty, coi) }
286

287
288
289
----------------------
boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI)
-- Special case for parrs
Ian Lynagh's avatar
Ian Lynagh committed
290
boxySplitPArrTy exp_ty
291
292
  = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty
       ; return (elt_ty, coi) }
293

294
----------------------
Ian Lynagh's avatar
Ian Lynagh committed
295
296
boxySplitAppTy :: BoxyRhoType                           -- Type to split: m a
               -> TcM ((BoxySigmaType, BoxySigmaType),  -- Returns m, a
297
                       CoercionI)
Ian Lynagh's avatar
Ian Lynagh committed
298
-- If the incoming type is a mutable type variable of kind k, then
299
-- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
300
-- If the incoming type is boxy, then so are the result types; and vice versa
301

302
303
304
boxySplitAppTy orig_ty
  = loop orig_ty
  where
Ian Lynagh's avatar
Ian Lynagh committed
305
    loop ty
306
307
      | Just ty' <- tcView ty = loop ty'

Ian Lynagh's avatar
Ian Lynagh committed
308
    loop ty
309
      | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
310
311
      = return ((fun_ty, arg_ty), IdCo)

312
    loop ty@(TyConApp tycon _args)
313
314
315
      | isOpenSynTyCon tycon        -- try to normalise type family application
      = do { (coi1, ty') <- tcNormaliseFamInst ty
           ; case coi1 of
Ian Lynagh's avatar
Ian Lynagh committed
316
               IdCo   -> defer    -- no progress, but maybe solvable => defer
Ian Lynagh's avatar
Ian Lynagh committed
317
               ACo _ ->          -- progress: so lets try again
Ian Lynagh's avatar
Ian Lynagh committed
318
319
320
                 do { (args, coi2) <- loop ty'
                    ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
                    }
321
           }
322
323

    loop (TyVarTy tv)
324
      | isTyConableTyVar tv
325
      = do { cts <- readMetaTyVar tv
Ian Lynagh's avatar
Ian Lynagh committed
326
327
328
329
           ; case cts of
               Indirect ty -> loop ty
               Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty
                           ; return ((fun_ty, arg_ty), IdCo) } }
330
331
      | otherwise             -- defer as tyvar may be refined by equalities
      = defer
332
      where
Ian Lynagh's avatar
Ian Lynagh committed
333
334
335
336
337
338
339
340
341
        tv_kind = tyVarKind tv
        kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
                                                -- m :: * -> k
                 liftedTypeKind]                -- arg type :: *
        -- The defaultKind is a bit smelly.  If you remove it,
        -- try compiling        f x = do { x }
        -- and you'll get a kind mis-match.  It smells, but
        -- not enough to lose sleep over.

342
    loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
343

344
345
346
347
348
    -- defer splitting by generating an equality constraint
    defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty
               ; return ((ty1, ty2), coi)
               }
      where
Ian Lynagh's avatar
Ian Lynagh committed
349
350
351
352
353
        orig_kind = typeKind orig_ty
        arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind),
                                                -- m :: * -> k
                     liftedTypeKind]            -- arg type :: *

354
355
356
357
    -- build type application
    mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
    mk_res_ty _other             = panic "TcUnify.mk_res_ty2"

358
------------------
Ian Lynagh's avatar
Ian Lynagh committed
359
boxySplitFailure :: TcType -> TcType -> TcM (a, CoercionI)
360
boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
361
362
363
364
365
366

------------------
boxySplitDefer :: [Kind]                   -- kinds of required arguments
               -> ([TcType] -> TcTauType)  -- construct lhs from argument tyvars
               -> BoxyRhoType              -- type to split
               -> TcM ([TcType], CoercionI)
367
boxySplitDefer kinds mk_ty orig_ty
368
  = do { tau_tys <- mapM newFlexiTyVarTy kinds
369
370
       ; let ty1 = mk_ty tau_tys
       ; coi <- defer_unification (Unify False ty1 orig_ty) False ty1 orig_ty
371
372
       ; return (tau_tys, coi)
       }
373
\end{code}
374
375


376
377
378
--------------------------------
-- withBoxes: the key utility function
--------------------------------
379

380
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
381
382
383
384
385
386
387
388
389
withMetaTvs :: TcTyVar  -- An unfilled-in, non-skolem, meta type variable
            -> [Kind]   -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
            -> ([BoxySigmaType] -> BoxySigmaType)
                                        -- Constructs the type to assign
                                        -- to the original var
            -> TcM [BoxySigmaType]      -- Return the fresh boxes

-- It's entirely possible for the [kind] to be empty.
-- For example, when pattern-matching on True,
390
391
392
393
394
395
-- we call boxySplitTyConApp passing a boolTyCon

-- Invariant: tv is still Flexi

withMetaTvs tv kinds mk_res_ty
  | isBoxyTyVar tv
Ian Lynagh's avatar
Ian Lynagh committed
396
397
398
399
  = do  { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
        ; let box_tys = mkTyVarTys box_tvs
        ; writeMetaTyVar tv (mk_res_ty box_tys)
        ; return box_tys }
400

Ian Lynagh's avatar
Ian Lynagh committed
401
402
403
404
405
  | otherwise                   -- Non-boxy meta type variable
  = do  { tau_tys <- mapM newFlexiTyVarTy kinds
        ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
                                                -- Sure to be a tau-type
        ; return tau_tys }
406
407
408
409

withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
-- Allocate a *boxy* tyvar
withBox kind thing_inside
Ian Lynagh's avatar
Ian Lynagh committed
410
411
412
413
  = do  { box_tv <- newBoxyTyVar kind
        ; res <- thing_inside (mkTyVarTy box_tv)
        ; ty  <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
        ; return (res, ty) }
414
\end{code}
415
416


417
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
418
419
420
%*                                                                      *
                Approximate boxy matching
%*                                                                      *
421
%************************************************************************
422

423
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
424
425
426
427
428
429
preSubType :: [TcTyVar]         -- Quantified type variables
           -> TcTyVarSet        -- Subset of quantified type variables
                                --   see Note [Pre-sub boxy]
            -> TcType           -- The rho-type part; quantified tyvars scopes over this
            -> BoxySigmaType    -- Matching type from the context
            -> TcM [TcType]     -- Types to instantiate the tyvars
430
431
-- Perform pre-subsumption, and return suitable types
-- to instantiate the quantified type varibles:
Ian Lynagh's avatar
Ian Lynagh committed
432
433
--      info from the pre-subsumption, if there is any
--      a boxy type variable otherwise
434
--
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
435
436
437
-- Note [Pre-sub boxy]
--   The 'btvs' are a subset of 'qtvs'.  They are the ones we can
--   instantiate to a boxy type variable, because they'll definitely be
Ian Lynagh's avatar
Ian Lynagh committed
438
439
440
441
--   filled in later.  This isn't always the case; sometimes we have type
--   variables mentioned in the context of the type, but not the body;
--                f :: forall a b. C a b => a -> a
--   Then we may land up with an unconstrained 'b', so we want to
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
442
443
444
445
--   instantiate it to a monotype (non-boxy) type variable
--
-- The 'qtvs' that are *neither* fixed by the pre-subsumption, *nor* are in 'btvs',
-- are instantiated to TauTv meta variables.
Ian Lynagh's avatar
Ian Lynagh committed
446

447
preSubType qtvs btvs qty expected_ty
448
  = do { tys <- mapM inst_tv qtvs
Ian Lynagh's avatar
Ian Lynagh committed
449
450
        ; traceTc (text "preSubType" <+> (ppr qtvs $$ ppr btvs $$ ppr qty $$ ppr expected_ty $$ ppr pre_subst $$ ppr tys))
        ; return tys }
451
452
  where
    pre_subst = boxySubMatchType (mkVarSet qtvs) qty expected_ty
Ian Lynagh's avatar
Ian Lynagh committed
453
454
455
456
457
458
459
460
461
462
463
    inst_tv tv
        | Just boxy_ty <- lookupTyVar pre_subst tv = return boxy_ty
        | tv `elemVarSet` btvs = do { tv' <- tcInstBoxyTyVar tv
                                    ; return (mkTyVarTy tv') }
        | otherwise            = do { tv' <- tcInstTyVar tv
                                    ; return (mkTyVarTy tv') }

boxySubMatchType
        :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
        -> BoxyRhoType          -- Type to match (note a *Rho* type)
        -> TvSubst              -- Substitution of the [TcTyVar] to BoxySigmaTypes
464

465
466
467
468
-- boxySubMatchType implements the Pre-subsumption judgement, in Fig 5 of the paper
-- "Boxy types: inference for higher rank types and impredicativity"

boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
469
  = go tmpl_tvs tmpl_ty emptyVarSet boxy_ty
470
  where
471
    go t_tvs t_ty b_tvs b_ty
Ian Lynagh's avatar
Ian Lynagh committed
472
473
        | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
        | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
474

Ian Lynagh's avatar
Ian Lynagh committed
475
    go _ (TyVarTy _) _ _ = emptyTvSubst      -- Rule S-ANY; no bindings
Ian Lynagh's avatar
Ian Lynagh committed
476
477
478
        -- Rule S-ANY covers (a) type variables and (b) boxy types
        -- in the template.  Both look like a TyVarTy.
        -- See Note [Sub-match] below
479

480
    go t_tvs t_ty b_tvs b_ty
Ian Lynagh's avatar
Ian Lynagh committed
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
        | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
        = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty       -- Rule S-SPEC
                -- Under a forall on the left, if there is shadowing,
                -- do not bind! Hence the delVarSetList.
        | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
        = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau      -- Rule S-SKOL
                -- Add to the variables we must not bind to
        -- NB: it's *important* to discard the theta part. Otherwise
        -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
        -- and end up with a completely bogus binding (b |-> Bool), by lining
        -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
        -- This pre-subsumption stuff can return too few bindings, but it
        -- must *never* return bogus info.

    go t_tvs (FunTy arg1 res1) b_tvs (FunTy arg2 res2)  -- Rule S-FUN
        = boxy_match t_tvs arg1 b_tvs arg2 (go t_tvs res1 b_tvs res2)
        -- Match the args, and sub-match the results
498

499
    go t_tvs t_ty b_tvs b_ty = boxy_match t_tvs t_ty b_tvs b_ty emptyTvSubst
Ian Lynagh's avatar
Ian Lynagh committed
500
501
        -- Otherwise defer to boxy matching
        -- This covers TyConApp, AppTy, PredTy
502
503
504
505
506
\end{code}

Note [Sub-match]
~~~~~~~~~~~~~~~~
Consider this
Ian Lynagh's avatar
Ian Lynagh committed
507
508
509
510
        head :: [a] -> a
        |- head xs : <rhobox>
We will do a boxySubMatchType between   a ~ <rhobox>
But we *don't* want to match [a |-> <rhobox>] because
511
    (a) The box should be filled in with a rho-type, but
Ian Lynagh's avatar
Ian Lynagh committed
512
513
           but the returned substitution maps TyVars to boxy
           *sigma* types
514
    (b) In any case, the right final answer might be *either*
Ian Lynagh's avatar
Ian Lynagh committed
515
516
           instantiate 'a' with a rho-type or a sigma type
           head xs : Int   vs   head xs : forall b. b->b
517
518
519
520
521
So the matcher MUST NOT make a choice here.   In general, we only
bind a template type variable in boxyMatchType, not in boxySubMatchType.


\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
522
523
524
525
boxyMatchTypes
        :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
        -> [BoxySigmaType]        -- Type to match
        -> TvSubst                -- Substitution of the [TcTyVar] to BoxySigmaTypes
526

527
528
529
-- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
-- "Boxy types: inference for higher rank types and impredicativity"

Ian Lynagh's avatar
Ian Lynagh committed
530
531
532
533
534
535
536
-- Find a *boxy* substitution that makes the template look as much
--      like the BoxySigmaType as possible.
-- It's always ok to return an empty substitution;
--      anything more is jam on the pudding
--
-- NB1: This is a pure, non-monadic function.
--      It does no unification, and cannot fail
537
538
--
-- Precondition: the arg lengths are equal
539
-- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
540
--
Ian Lynagh's avatar
Ian Lynagh committed
541

542
543
544
545
------------
boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
  = ASSERT( length tmpl_tys == length boxy_tys )
    boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
Ian Lynagh's avatar
Ian Lynagh committed
546
        -- ToDo: add error context?
547

Ian Lynagh's avatar
Ian Lynagh committed
548
549
550
boxy_match_s :: TcTyVarSet -> [TcType] -> TcTyVarSet -> [BoxySigmaType]
             -> TvSubst -> TvSubst
boxy_match_s _ [] _ [] subst
551
552
  = subst
boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
553
554
  = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
    boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
Ian Lynagh's avatar
Ian Lynagh committed
555
boxy_match_s _ _ _ _ _
Ian Lynagh's avatar
Ian Lynagh committed
556
557
  = panic "boxy_match_s"        -- Lengths do not match

558
559

------------
Ian Lynagh's avatar
Ian Lynagh committed
560
561
562
563
564
boxy_match :: TcTyVarSet -> TcType      -- Template
           -> TcTyVarSet                -- boxy_tvs: do not bind template tyvars to any of these
           -> BoxySigmaType             -- Match against this type
           -> TvSubst
           -> TvSubst
565
566

-- The boxy_tvs argument prevents this match:
Ian Lynagh's avatar
Ian Lynagh committed
567
--      [a]  forall b. a  ~  forall b. b
568
569
570
571
572
573
-- We don't want to bind the template variable 'a'
-- to the quantified type variable 'b'!

boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
  = go orig_tmpl_ty orig_boxy_ty
  where
Ian Lynagh's avatar
Ian Lynagh committed
574
575
576
577
578
579
580
581
582
583
584
    go t_ty b_ty
        | Just t_ty' <- tcView t_ty = go t_ty' b_ty
        | Just b_ty' <- tcView b_ty = go t_ty b_ty'

    go ty1 ty2          -- C.f. the isSigmaTy case for boxySubMatchType
        | isSigmaTy ty1
        , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
        , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
        , equalLength tvs1 tvs2
        = boxy_match (tmpl_tvs `delVarSetList` tvs1)    tau1
                     (boxy_tvs `extendVarSetList` tvs2) tau2 subst
585
586

    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
Ian Lynagh's avatar
Ian Lynagh committed
587
588
589
        | tc1 == tc2
        , not $ isOpenSynTyCon tc1
        = go_s tys1 tys2
590
591

    go (FunTy arg1 res1) (FunTy arg2 res2)
Ian Lynagh's avatar
Ian Lynagh committed
592
        = go_s [arg1,res1] [arg2,res2]
593
594

    go t_ty b_ty
Ian Lynagh's avatar
Ian Lynagh committed
595
596
597
598
        | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
          Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
          typeKind t2 `isSubKind` typeKind t1   -- Maintain invariant
        = go_s [s1,t1] [s2,t2]
599
600

    go (TyVarTy tv) b_ty
Ian Lynagh's avatar
Ian Lynagh committed
601
602
603
604
605
606
607
608
609
610
        | tv `elemVarSet` tmpl_tvs      -- Template type variable in the template
        , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
        , typeKind b_ty `isSubKind` tyVarKind tv  -- See Note [Matching kinds]
        = extendTvSubst subst tv boxy_ty'
        | otherwise
        = subst                         -- Ignore others
        where
          boxy_ty' = case lookupTyVar subst tv of
                        Nothing -> orig_boxy_ty
                        Just ty -> ty `boxyLub` orig_boxy_ty
611

612
    go _ (TyVarTy tv) | isMetaTyVar tv
Ian Lynagh's avatar
Ian Lynagh committed
613
614
615
616
617
618
619
620
621
622
623
624
        = subst         -- Don't fail if the template has more info than the target!
                        -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                        -- would fail to instantiate 'a', because the meta-type-variable
                        -- beta is as yet un-filled-in

    go _ _ = emptyTvSubst       -- It's important to *fail* by returning the empty substitution
        -- Example:  Tree a ~ Maybe Int
        -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
        -- misleading error messages.  An even more confusing case is
        --           a -> b ~ Maybe Int
        -- Then we do not want to bind (b |-> Int)!  It's always safe to discard bindings
        -- from this pre-matching phase.
625
626
627
628
629
630
631
632
633
634
635
636

    --------
    go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst


boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
-- Combine boxy information from the two types
-- If there is a conflict, return the first
boxyLub orig_ty1 orig_ty2
  = go orig_ty1 orig_ty2
  where
    go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
637
    go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
Ian Lynagh's avatar
Ian Lynagh committed
638
    go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
639
640
641
      | tc1 == tc2, length ts1 == length ts2
      = TyConApp tc1 (zipWith boxyLub ts1 ts2)

Ian Lynagh's avatar
Ian Lynagh committed
642
    go (TyVarTy tv1) _                  -- This is the whole point;
Ian Lynagh's avatar
Ian Lynagh committed
643
644
      | isTcTyVar tv1, isBoxyTyVar tv1  -- choose ty2 if ty2 is a box
      = orig_ty2
645

Ian Lynagh's avatar
Ian Lynagh committed
646
    go _ (TyVarTy tv2)                -- Symmetrical case
647
      | isTcTyVar tv2, isBoxyTyVar tv2
Ian Lynagh's avatar
Ian Lynagh committed
648
      = orig_ty1
649

Ian Lynagh's avatar
Ian Lynagh committed
650
        -- Look inside type synonyms, but only if the naive version fails
651
    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
Ian Lynagh's avatar
Ian Lynagh committed
652
               | Just ty2' <- tcView ty1 = go ty1 ty2'
653
654

    -- For now, we don't look inside ForAlls, PredTys
Ian Lynagh's avatar
Ian Lynagh committed
655
    go _ _ = orig_ty1       -- Default
656
657
\end{code}

658
659
Note [Matching kinds]
~~~~~~~~~~~~~~~~~~~~~
Ian Lynagh's avatar
Ian Lynagh committed
660
661
662
The target type might legitimately not be a sub-kind of template.
For example, suppose the target is simply a box with an OpenTypeKind,
and the template is a type variable with LiftedTypeKind.
663
664
665
666
667
668
669
670
Then it's ok (because the target type will later be refined).
We simply don't bind the template type variable.

It might also be that the kind mis-match is an error. For example,
suppose we match the template (a -> Int) against (Int# -> Int),
where the template type variable 'a' has LiftedTypeKind.  This
matching function does not fail; it simply doesn't bind the template.
Later stuff will fail.
671

672
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
673
674
675
%*                                                                      *
                Subsumption checking
%*                                                                      *
676
677
%************************************************************************

678
All the tcSub calls have the form
Ian Lynagh's avatar
Ian Lynagh committed
679
680

                tcSub actual_ty expected_ty
681
which checks
Ian Lynagh's avatar
Ian Lynagh committed
682
                actual_ty <= expected_ty
683

684
That is, that a value of type actual_ty is acceptable in
685
686
a place expecting a value of type expected_ty.

Ian Lynagh's avatar
Ian Lynagh committed
687
688
It returns a coercion function
        co_fn :: actual_ty ~ expected_ty
689
which takes an HsExpr of type actual_ty into one of type
690
691
692
expected_ty.

\begin{code}
693
-----------------
694
tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
Ian Lynagh's avatar
Ian Lynagh committed
695
696
        -- (tcSub act exp) checks that
        --      act <= exp
697
tcSubExp orig actual_ty expected_ty
698
699
  = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
    -- Adding the error context here leads to some very confusing error
700
    -- messages, such as "can't match forall a. a->a with forall a. a->a"
Ian Lynagh's avatar
Ian Lynagh committed
701
702
    -- Example is tcfail165:
    --      do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String))
703
704
705
706
707
708
    --         putMVar var (show :: forall a. Show a => a -> String)
    -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg
    -- but after zonking it looks as if it does!
    --
    -- So instead I'm adding the error context when moving from tc_sub to u_tys

709
    traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
710
    tc_sub orig actual_ty actual_ty False expected_ty expected_ty
711

712
-----------------
713
tc_sub :: InstOrigin
Ian Lynagh's avatar
Ian Lynagh committed
714
715
716
717
718
       -> BoxySigmaType         -- actual_ty, before expanding synonyms
       -> BoxySigmaType         --              ..and after
       -> InBox                 -- True <=> expected_ty is inside a box
       -> BoxySigmaType         -- expected_ty, before
       -> BoxySigmaType         --              ..and after
719
       -> TcM HsWrapper
Ian Lynagh's avatar
Ian Lynagh committed
720
721
722
723
                                -- The acual_ty is never inside a box
-- IMPORTANT pre-condition: if the args contain foralls, the bound type
--                          variables are visible non-monadically
--                          (i.e. tha args are sufficiently zonked)
724
-- This invariant is needed so that we can "see" the foralls, ad
Ian Lynagh's avatar
Ian Lynagh committed
725
726
-- e.g. in the SPEC rule where we just use splitSigmaTy

727
tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
728
  = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
729
    tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
Ian Lynagh's avatar
Ian Lynagh committed
730
731
        -- This indirection is just here to make
        -- it easy to insert a debug trace!
732

Ian Lynagh's avatar
Ian Lynagh committed
733
734
tc_sub1 :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> InBox
        -> BoxySigmaType -> Type -> TcM HsWrapper
735
736
737
738
tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
  | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
  | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty
739

740
-----------------------------------
741
742
743
-- Rule SBOXY, plus other cases when act_ty is a type variable
-- Just defer to boxy matching
-- This rule takes precedence over SKOL!
744
tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
Ian Lynagh's avatar
Ian Lynagh committed
745
746
747
748
749
750
751
752
  = do  { traceTc (text "tc_sub1 - case 1")
        ; coi <- addSubCtxt orig act_sty exp_sty $
                 uVar (Unify True act_sty exp_sty) False tv exp_ib exp_sty exp_ty
        ; traceTc (case coi of
                        IdCo   -> text "tc_sub1 (Rule SBOXY) IdCo"
                        ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
        ; return $ coiToHsWrapper coi
        }
753
754

-----------------------------------
755
-- Skolemisation case (rule SKOL)
Ian Lynagh's avatar
Ian Lynagh committed
756
757
758
--      actual_ty:   d:Eq b => b->b
--      expected_ty: forall a. Ord a => a->a
--      co_fn e      /\a. \d2:Ord a. let d = eqFromOrd d2 in e
759
760
761

-- It is essential to do this *before* the specialisation case
-- Example:  f :: (Eq a => a->a) -> ...
Ian Lynagh's avatar
Ian Lynagh committed
762
--           g :: Ord b => b->b
763
764
-- Consider  f g !

765
tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
766
767
  | isSigmaTy exp_ty = do
    { traceTc (text "tc_sub1 - case 2") ;
Ian Lynagh's avatar
Ian Lynagh committed
768
769
770
771
772
773
    if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
        defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
    else do
        { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
                             tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
        ; return (gen_fn <.> co_fn) }
774
    }
775
776
  where
    act_tvs = tyVarsOfType act_ty
Ian Lynagh's avatar
Ian Lynagh committed
777
778
                -- It's really important to check for escape wrt
                -- the free vars of both expected_ty *and* actual_ty
779
780

-----------------------------------
781
-- Specialisation case (rule ASPEC):
Ian Lynagh's avatar
Ian Lynagh committed
782
783
784
--      actual_ty:   forall a. Ord a => a->a
--      expected_ty: Int -> Int
--      co_fn e =    e Int dOrdInt
785

Ian Lynagh's avatar
Ian Lynagh committed
786
tc_sub1 orig _ actual_ty exp_ib exp_sty expected_ty
787
788
789
790
-- Implements the new SPEC rule in the Appendix of the paper
-- "Boxy types: inference for higher rank types and impredicativity"
-- (This appendix isn't in the published version.)
-- The idea is to *first* do pre-subsumption, and then full subsumption
Ian Lynagh's avatar
Ian Lynagh committed
791
-- Example:     forall a. a->a  <=  Int -> (forall b. Int)
792
793
--   Pre-subsumpion finds a|->Int, and that works fine, whereas
--   just running full subsumption would fail.
794
  | isSigmaTy actual_ty
Ian Lynagh's avatar
Ian Lynagh committed
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
  = do  { traceTc (text "tc_sub1 - case 3")
        ;       -- Perform pre-subsumption, and instantiate
                -- the type with info from the pre-subsumption;
                -- boxy tyvars if pre-subsumption gives no info
          let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty
              tau_tvs = exactTyVarsOfType tau
        ; inst_tys <- if exp_ib then    -- Inside a box, do not do clever stuff
                        do { tyvars' <- mapM tcInstBoxyTyVar tyvars
                           ; return (mkTyVarTys tyvars') }
                      else              -- Outside, do clever stuff
                        preSubType tyvars tau_tvs tau expected_ty
        ; let subst' = zipOpenTvSubst tyvars inst_tys
              tau'   = substTy subst' tau

                -- Perform a full subsumption check
        ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
                                                ppr tyvars <+> ppr theta <+> ppr tau,
                                                ppr tau'])
        ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty

                -- Deal with the dictionaries
        ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
        ; return (co_fn2 <.> co_fn1) }
818
819

-----------------------------------
820
-- Function case (rule F1)
Ian Lynagh's avatar
Ian Lynagh committed
821
tc_sub1 orig _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res)
822
  = do { traceTc (text "tc_sub1 - case 4")
823
       ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
824
       }
825
826

-- Function case (rule F2)
827
tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
828
  | isBoxyTyVar exp_tv
Ian Lynagh's avatar
Ian Lynagh committed
829
830
831
832
833
834
  = do  { traceTc (text "tc_sub1 - case 5")
        ; cts <- readMetaTyVar exp_tv
        ; case cts of
            Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty
            Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
                        ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
835
836
 where
    mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
Ian Lynagh's avatar
Ian Lynagh committed
837
    mk_res_ty _ = panic "TcUnify.mk_res_ty3"
838
839
840
    fun_kinds = [argTypeKind, openTypeKind]

-- Everything else: defer to boxy matching
841
tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
842
  = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
843
       ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
844
845
       }

846
tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
847
  = do { traceTc (text "tc_sub1 - case 6")
848
       ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
849
       }
850
851

-----------------------------------
Ian Lynagh's avatar
Ian Lynagh committed
852
853
defer_to_boxy_matching :: InstOrigin -> TcType -> TcType -> InBox
                       -> TcType -> TcType -> TcM HsWrapper
854
defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
Ian Lynagh's avatar
Ian Lynagh committed
855
856
857
858
  = do  { coi <- addSubCtxt orig act_sty exp_sty $
                 u_tys (Unify True act_sty exp_sty)
                       False act_sty actual_ty exp_ib exp_sty expected_ty
        ; return $ coiToHsWrapper coi }
859
860

-----------------------------------
Ian Lynagh's avatar
Ian Lynagh committed
861
862
tc_sub_funs :: InstOrigin -> TcType -> BoxySigmaType -> InBox
            -> TcType -> BoxySigmaType -> TcM HsWrapper
863
tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
Ian Lynagh's avatar
Ian Lynagh committed
864
865
866
867
868
869
870
871
  = do  { arg_coi   <- addSubCtxt orig act_arg exp_arg $
                       uTysOuter False act_arg exp_ib exp_arg
        ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
        ; wrapper1  <- wrapFunResCoercion [exp_arg] co_fn_res
        ; let wrapper2 = case arg_coi of
                                IdCo   -> idHsWrapper
                                ACo co -> WpCast $ FunTy co act_res
        ; return (wrapper1 <.> wrapper2) }
872
873

-----------------------------------
Ian Lynagh's avatar
Ian Lynagh committed
874
875
876
877
wrapFunResCoercion
        :: [TcType]     -- Type of args
        -> HsWrapper    -- HsExpr a -> HsExpr b
        -> TcM HsWrapper        -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
878
wrapFunResCoercion arg_tys co_fn_res
Ian Lynagh's avatar
Ian Lynagh committed
879
  | isIdHsWrapper co_fn_res
880
  = return idHsWrapper
Ian Lynagh's avatar
Ian Lynagh committed
881
  | null arg_tys
882
  = return co_fn_res
883
  | otherwise
Ian Lynagh's avatar
Ian Lynagh committed
884
885
  = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
        ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
886
887
888
\end{code}


889

890
%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
891
%*                                                                      *
892
\subsection{Generalisation}
Ian Lynagh's avatar
Ian Lynagh committed
893
%*                                                                      *
894
895
896
%************************************************************************

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
897
898
899
900
tcGen :: BoxySigmaType                          -- expected_ty
      -> TcTyVarSet                             -- Extra tyvars that the universally
                                                --      quantified tyvars of expected_ty
                                                --      must not be unified
901
      -> ([TcTyVar] -> BoxyRhoType -> TcM result)
902
      -> TcM (HsWrapper, result)
Ian Lynagh's avatar
Ian Lynagh committed
903
904
905
906
907
908
909
910
911
912
913
914
915
916
        -- The expression has type: spec_ty -> expected_ty

tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
                                                -- If not, the call is a no-op
  = do  { traceTc (text "tcGen")
                -- We want the GenSkol info in the skolemised type variables to
                -- mention the *instantiated* tyvar names, so that we get a
                -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
                -- Hence the tiresome but innocuous fixM
        ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
                do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
                        -- Get loation from monad, not from expected_ty
                   ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
                   ; return ((forall_tvs, theta, rho_ty), skol_info) })
917

Ian Lynagh's avatar
Ian Lynagh committed
918
919
920
921
922
923
924
        ; when debugIsOn $
              traceTc (text "tcGen" <+> vcat [
                           text "extra_tvs" <+> ppr extra_tvs,
                           text "expected_ty" <+> ppr expected_ty,
                           text "inst ty" <+> ppr tvs' <+> ppr theta'
                               <+> ppr rho',
                           text "free_tvs" <+> ppr free_tvs])
925

Ian Lynagh's avatar
Ian Lynagh committed
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
        -- Type-check the arg and unify with poly type
        ; (result, lie) <- getLIE (thing_inside tvs' rho')

        -- Check that the "forall_tvs" havn't been constrained
        -- The interesting bit here is that we must include the free variables
        -- of the expected_ty.  Here's an example:
        --       runST (newVar True)
        -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
        -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
        -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
        -- So now s' isn't unconstrained because it's linked to a.
        -- Conclusion: include the free vars of the expected_ty in the
        -- list of "free vars" for the signature check.

        ; loc <- getInstLoc (SigOrigin skol_info)
        ; dicts <- newDictBndrs loc theta'      -- Includes equalities
        ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie

        ; checkSigTyVarsWrt free_tvs tvs'
        ; traceTc (text "tcGen:done")

        ; let
            -- The WpLet binds any Insts which came out of the simplification.
            dict_vars = map instToVar dicts
            co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
        ; return (co_fn, result) }
952
  where
953
    free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
954
\end{code}
955

Ian Lynagh's avatar
Ian Lynagh committed
956

957
958

%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
959
960
961
%*                                                                      *
                Boxy unification
%*                                                                      *
962
963
964
965
966
967
%************************************************************************

The exported functions are all defined as versions of some
non-exported generic functions.

\begin{code}
968
boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
969
-- Acutal and expected, respectively
970
boxyUnify ty1 ty2 = addErrCtxtM (unifyCtxt ty1 ty2) $
Ian Lynagh's avatar
Ian Lynagh committed
971
                    uTysOuter False ty1 False ty2
972
973

---------------
Ian Lynagh's avatar
Ian Lynagh committed
974
boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
975
976
977
978
979
-- Arguments should have equal length
-- Acutal and expected types
boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2

---------------
980
unifyType :: TcTauType -> TcTauType -> TcM CoercionI
981
982
-- No boxes expected inside these types
-- Acutal and expected types
Ian Lynagh's avatar
Ian Lynagh committed
983
unifyType ty1 ty2       -- ty1 expected, ty2 inferred
984
985
  = ASSERT2( not (isBoxyTy ty1), ppr ty1 )
    ASSERT2( not (isBoxyTy ty2), ppr ty2 )
986
987
    addErrCtxtM (unifyCtxt ty1 ty2) $
    uTysOuter True ty1 True ty2
988
989

---------------
990
unifyPred :: PredType -> PredType -> TcM CoercionI
991
-- Acutal and expected types
992
unifyPred p1 p2 = uPred (Unify False (mkPredTy p1) (mkPredTy p2)) True p1 True p2
993

994
unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
995
-- Acutal and expected types
996
unifyTheta theta1 theta2
Ian Lynagh's avatar
Ian Lynagh committed
997
998
  = do  { checkTc (equalLength theta1 theta2)
                  (vcat [ptext (sLit "Contexts differ in length"),
999
                         nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
Ian Lynagh's avatar
Ian Lynagh committed
1000
        ; uList unifyPred theta1 theta2
1001
        }
1002
1003

---------------
1004
1005
uList :: (a -> a -> TcM b)
       -> [a] -> [a] -> TcM [b]
1006
-- Unify corresponding elements of two lists of types, which
1007
-- should be of equal length.  We charge down the list explicitly so that
1008
-- we can complain if their lengths differ.
Ian Lynagh's avatar
Ian Lynagh committed
1009
uList _     []         []         = return []
Ian Lynagh's avatar
Ian Lynagh committed
1010
1011
1012
1013
uList unify (ty1:tys1) (ty2:tys2) = do { x  <- unify ty1 ty2;
                                       ; xs <- uList unify tys1 tys2
                                       ; return (x:xs)
                                       }
Ian Lynagh's avatar
Ian Lynagh committed
1014
uList _ _ _ = panic "Unify.uList: mismatched type lists!"
1015
1016
\end{code}

1017
@unifyTypeList@ takes a single list of @TauType@s and unifies them
1018
1019
1020
1021
all together.  It is used, for example, when typechecking explicit
lists, when all the elts should be of the same type.

\begin{code}
1022
unifyTypeList :: [TcTauType] -> TcM ()
Ian Lynagh's avatar
Ian Lynagh committed
1023
unifyTypeList []                 = return ()
Ian Lynagh's avatar
Ian Lynagh committed
1024
unifyTypeList [_]                = return ()
1025
unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
Ian Lynagh's avatar
Ian Lynagh committed
1026
                                      ; unifyTypeList tys }
1027
1028
1029
\end{code}

%************************************************************************
Ian Lynagh's avatar
Ian Lynagh committed
1030
%*                                                                      *
1031
\subsection[Unify-uTys]{@uTys@: getting down to business}
Ian Lynagh's avatar
Ian Lynagh committed
1032
%*                                                                      *
1033
1034
%************************************************************************

1035
1036
@uTys@ is the heart of the unifier.  Each arg occurs twice, because
we want to report errors in terms of synomyms if possible.  The first of
1037
1038
1039
1040
1041
1042
1043
the pair is used in error messages only; it is always the same as the
second, except that if the first is a synonym then the second may be a
de-synonym'd version.  This way we get better error messages.

We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.

\begin{code}
1044
type SwapFlag = Bool
Ian Lynagh's avatar
Ian Lynagh committed
1045
1046
        -- False <=> the two args are (actual, expected) respectively
        -- True  <=> the two args are (expected, actual) respectively
1047

Ian Lynagh's avatar
Ian Lynagh committed
1048
1049
1050
1051
1052
1053
type InBox = Bool       -- True  <=> we are inside a box
                        -- False <=> we are outside a box
        -- The importance of this is that if we get "filled-box meets
        -- filled-box", we'll look into the boxes and unify... but
        -- we must not allow polytypes.  But if we are in a box on
        -- just one side, then we can allow polytypes
1054

Ian Lynagh's avatar
Ian Lynagh committed
1055
1056
1057
1058
data Outer = Unify Bool TcType TcType
        -- If there is a unification error, report these types as mis-matching
        -- Bool = True <=> the context says "Expected = ty1, Acutal = ty2"
        --                 for this particular ty1,ty2
1059

1060
instance Outputable Outer where
1061
  ppr (Unify c ty1 ty2) = pp_c <+> pprParendType ty1 <+> ptext (sLit "~")
Ian Lynagh's avatar
Ian Lynagh committed
1062
1063
1064
1065
                               <+> pprParendType ty2
        where
          pp_c = if c then ptext (sLit "Top") else ptext (sLit "NonTop")

1066
1067

-------------------------
Ian Lynagh's avatar
Ian Lynagh committed
1068
1069
1070
uTysOuter :: InBox -> TcType    -- ty1 is the *actual*   type
          -> InBox -> TcType    -- ty2 is the *expected* type
          -> TcM CoercionI
1071
-- We've just pushed a context describing ty1,ty2
Ian Lynagh's avatar
Ian Lynagh committed
1072
1073
1074
uTysOuter nb1 ty1 nb2 ty2
        = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
             ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
1075
1076
1077

uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
-- The context does not describe ty1,ty2
Ian Lynagh's avatar
Ian Lynagh committed