TcUnify.hs 67.7 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5 6

Type subsumption and unification
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
9
{-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

11
module TcUnify (
dreixel's avatar
dreixel committed
12
  -- Full-blown subsumption
13 14 15
  tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
  tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
  tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC,
16
  checkConstraints, buildImplicationFor,
17

dreixel's avatar
dreixel committed
18
  -- Various unifications
Simon Peyton Jones's avatar
Simon Peyton Jones committed
19
  unifyType, unifyTheta, unifyKind, noThing,
20
  uType, unifyExpType,
21
  swapOverTyVars, canSolveByUnification,
22

23 24
  --------------------------------
  -- Holes
batterseapower's avatar
batterseapower committed
25 26 27 28
  tcInfer,
  matchExpectedListTy,
  matchExpectedPArrTy,
  matchExpectedTyConApp,
29
  matchExpectedAppTy,
batterseapower's avatar
batterseapower committed
30
  matchExpectedFunTys,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
31
  matchActualFunTys, matchActualFunTysPart,
batterseapower's avatar
batterseapower committed
32
  matchExpectedFunKind,
33

Simon Peyton Jones's avatar
Simon Peyton Jones committed
34
  wrapFunResCoercion
dreixel's avatar
dreixel committed
35

36 37 38 39
  ) where

#include "HsVersions.h"

40
import HsSyn
41
import TyCoRep
42
import TcMType
43
import TcRnMonad
44 45
import TcType
import Type
46
import Coercion
47
import TcEvidence
dreixel's avatar
dreixel committed
48
import Name ( isSystemName )
49 50 51 52
import Inst
import TyCon
import TysWiredIn
import Var
53
import VarSet
54
import VarEnv
55
import ErrUtils
56
import DynFlags
57
import BasicTypes
58
import Name   ( Name )
59
import Bag
60
import Util
61
import Outputable
62
import FastString
63 64

import Control.Monad
65
import Control.Arrow ( second )
66

Austin Seipp's avatar
Austin Seipp committed
67 68 69
{-
************************************************************************
*                                                                      *
70
             matchExpected functions
Austin Seipp's avatar
Austin Seipp committed
71 72
*                                                                      *
************************************************************************
73

74 75 76 77 78 79 80
Note [Herald for matchExpectedFunTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The 'herald' always looks like:
   "The equation(s) for 'f' have"
   "The abstraction (\x.e) takes"
   "The section (+ x) expects"
   "The function 'f' is applied to"
81

82
This is used to construct a message of form
83

84
   The abstraction `\Just 1 -> ...' takes two arguments
85 86 87 88 89 90 91 92 93 94 95
   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

96 97
Note [matchExpectedFunTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
98
matchExpectedFunTys checks that a sigma has the form
99 100 101 102 103
of an n-ary function.  It passes the decomposed type to the
thing_inside, and returns a wrapper to coerce between the two types

It's used wherever a language construct must have a functional type,
namely:
104 105
        A lambda expression
        A function definition
106 107
     An operator section

108 109 110 111
This function must be written CPS'd because it needs to fill in the
ExpTypes produced for arguments before it can fill in the ExpType
passed in.

Austin Seipp's avatar
Austin Seipp committed
112
-}
113

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
114 115
-- Use this one when you have an "expected" type.
matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
116
                    -> Arity
117 118 119 120 121 122 123 124 125 126 127
                    -> ExpRhoType  -- deeply skolemised
                    -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
                          -- must fill in these ExpTypes here
                    -> TcM (a, HsWrapper)
-- If    matchExpectedFunTys n ty = (_, wrap)
-- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty,
--   where [t1, ..., tn], ty_r are passed to the thing_inside
matchExpectedFunTys herald arity orig_ty thing_inside
  = case orig_ty of
      Check ty -> go [] arity ty
      _        -> defer [] arity orig_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
128
  where
129 130 131 132 133 134 135
    go acc_arg_tys 0 ty
      = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty)
           ; return (result, idHsWrapper) }

    go acc_arg_tys n ty
      | Just ty' <- coreView ty = go acc_arg_tys n ty'

Simon Peyton Jones's avatar
Simon Peyton Jones committed
136
    go acc_arg_tys n (FunTy arg_ty res_ty)
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
      = ASSERT( not (isPredTy arg_ty) )
        do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
                                      (n-1) res_ty
           ; return ( result
                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty ) }

    go acc_arg_tys n ty@(TyVarTy tv)
      | ASSERT( isTcTyVar tv) isMetaTyVar tv
      = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty' -> go acc_arg_tys n ty'
               Flexi        -> defer acc_arg_tys n (mkCheckExpType ty) }

       -- In all other cases we bale out into ordinary unification
       -- However unlike the meta-tyvar case, we are sure that the
       -- number of arguments doesn't match arity of the original
       -- type, so we can add a bit more context to the error message
       -- (cf Trac #7869).
       --
       -- It is not always an error, because specialized type may have
       -- different arity, for example:
       --
       -- > f1 = f2 'a'
       -- > f2 :: Monad m => m Bool
       -- > f2 = undefined
       --
       -- But in that case we add specialized type into error context
       -- anyway, because it may be useful. See also Trac #9605.
    go acc_arg_tys n ty = addErrCtxtM mk_ctxt $
                          defer acc_arg_tys n (mkCheckExpType ty)

    ------------
    defer acc_arg_tys n fun_ty
      = do { more_arg_tys <- replicateM n newOpenInferExpType
           ; res_ty       <- newOpenInferExpType
           ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
           ; more_arg_tys <- mapM readExpType more_arg_tys
           ; res_ty       <- readExpType res_ty
           ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
           ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty
           ; return (result, wrap) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
178

179 180 181 182 183 184 185 186 187 188 189
    ------------
    mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc)
    mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_tc_ty
                     ; let (args, _) = tcSplitFunTys ty
                           n_actual = length args
                           (env'', orig_ty') = tidyOpenType env' orig_tc_ty
                     ; return ( env''
                              , mk_fun_tys_msg orig_ty' ty n_actual arity herald) }
      where
        orig_tc_ty = checkingExpType "matchExpectedFunTys" orig_ty
            -- this is safe b/c we're called from "go"
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
190

191 192 193 194
-- Like 'matchExpectedFunTys', but used when you have an "actual" type,
-- for example in function application
matchActualFunTys :: Outputable a
                  => SDoc   -- See Note [Herald for matchExpectedFunTys]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
195
                  -> CtOrigin
196
                  -> Maybe a   -- the thing with type TcSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
197 198 199
                  -> Arity
                  -> TcSigmaType
                  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
200 201 202 203
-- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
-- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
matchActualFunTys herald ct_orig mb_thing arity ty
  = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
204 205 206

-- | Variant of 'matchActualFunTys' that works when supplied only part
-- (that is, to the right of some arrows) of the full function type
207 208
matchActualFunTysPart :: Outputable a
                      => SDoc -- See Note [Herald for matchExpectedFunTys]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
209
                      -> CtOrigin
210
                      -> Maybe a  -- the thing with type TcSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
211 212 213 214 215
                      -> Arity
                      -> TcSigmaType
                      -> [TcSigmaType] -- reversed args. See (*) below.
                      -> Arity   -- overall arity of the function, for errs
                      -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
216 217
matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
                      orig_old_args full_arity
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
218
  = go arity orig_old_args orig_ty
219 220
-- Does not allocate unnecessary meta variables: if the input already is
-- a function, we just take it apart.  Not only is this efficient,
221
-- it's important for higher rank: the argument might be of form
222
--              (forall a. ty) -> other
223 224 225
-- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
-- hide the forall inside a meta-variable

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
226 227 228 229 230
-- (*) Sometimes it's necessary to call matchActualFunTys with only part
-- (that is, to the right of some arrows) of the type of the function in
-- question. (See TcExpr.tcArgs.) This argument is the reversed list of
-- arguments already seen (that is, not part of the TcSigmaType passed
-- in elsewhere).
231

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
  where
    -- This function has a bizarre mechanic: it accumulates arguments on
    -- the way down and also builds an argument list on the way up. Why:
    -- 1. The returns args list and the accumulated args list might be different.
    --    The accumulated args include all the arg types for the function,
    --    including those from before this function was called. The returned
    --    list should include only those arguments produced by this call of
    --    matchActualFunTys
    --
    -- 2. The HsWrapper can be built only on the way up. It seems (more)
    --    bizarre to build the HsWrapper but not the arg_tys.
    --
    -- Refactoring is welcome.
    go :: Arity
       -> [TcSigmaType] -- accumulator of arguments (reversed)
       -> TcSigmaType   -- the remainder of the type as we're processing
       -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
    go 0 _ ty = return (idHsWrapper, [], ty)

    go n acc_args ty
      | not (null tvs && null theta)
      = do { (wrap1, rho) <- topInstantiate ct_orig ty
           ; (wrap2, arg_tys, res_ty) <- go n acc_args rho
           ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
      where
        (tvs, theta, _) = tcSplitSigmaTy ty
258

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
259 260
    go n acc_args ty
      | Just ty' <- coreView ty = go n acc_args ty'
261

Simon Peyton Jones's avatar
Simon Peyton Jones committed
262
    go n acc_args (FunTy arg_ty res_ty)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
263 264
      = ASSERT( not (isPredTy arg_ty) )
        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
265 266
           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r
                    , arg_ty : tys, ty_r ) }
267

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
268
    go n acc_args ty@(TyVarTy tv)
269 270
      | ASSERT( isTcTyVar tv) isMetaTyVar tv
      = do { cts <- readMetaTyVar tv
271
           ; case cts of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
272
               Indirect ty' -> go n acc_args ty'
273
               Flexi        -> defer n ty }
274 275

       -- In all other cases we bale out into ordinary unification
276
       -- However unlike the meta-tyvar case, we are sure that the
277 278 279 280 281 282 283 284 285 286 287 288 289
       -- number of arguments doesn't match arity of the original
       -- type, so we can add a bit more context to the error message
       -- (cf Trac #7869).
       --
       -- It is not always an error, because specialized type may have
       -- different arity, for example:
       --
       -- > f1 = f2 'a'
       -- > f2 :: Monad m => m Bool
       -- > f2 = undefined
       --
       -- But in that case we add specialized type into error context
       -- anyway, because it may be useful. See also Trac #9605.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
290
    go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
291
                       defer n ty
292 293

    ------------
294 295 296
    defer n fun_ty
      = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
           ; res_ty  <- newOpenFlexiTyVarTy
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
297
           ; let unif_fun_ty = mkFunTys arg_tys res_ty
298
           ; co <- unifyType mb_thing fun_ty unif_fun_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
299
           ; return (mkWpCastN co, arg_tys, res_ty) }
300 301

    ------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
302 303 304 305 306 307 308 309
    mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
    mk_ctxt arg_tys res_ty env
      = do { let ty = mkFunTys arg_tys res_ty
           ; (env1, zonked) <- zonkTidyTcType env ty
                   -- zonking might change # of args
           ; let (zonked_args, _) = tcSplitFunTys zonked
                 n_actual         = length zonked_args
                 (env2, unzonked) = tidyOpenType env1 ty
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
           ; return ( env2
                    , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) }

mk_fun_tys_msg :: TcType  -- the full type passed in (unzonked)
               -> TcType  -- the full type passed in (zonked)
               -> Arity   -- the # of args found
               -> Arity   -- the # of args wanted
               -> SDoc    -- overall herald
               -> SDoc
mk_fun_tys_msg full_ty ty n_args full_arity herald
  = herald <+> speakNOf full_arity (text "argument") <> comma $$
    if n_args == full_arity
      then text "its type is" <+> quotes (pprType full_ty) <>
           comma $$
           text "it is specialized to" <+> quotes (pprType ty)
      else sep [text "but its type" <+> quotes (pprType ty),
                if n_args == 0 then text "has none"
                else text "has only" <+> speakN n_args]
328

329
----------------------
330
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
331
-- Special case for lists
332
matchExpectedListTy exp_ty
batterseapower's avatar
batterseapower committed
333 334
 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
      ; return (co, elt_ty) }
335

336
----------------------
337
matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
338
-- Special case for parrs
339
matchExpectedPArrTy exp_ty
batterseapower's avatar
batterseapower committed
340 341
  = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
       ; return (co, elt_ty) }
342

343
---------------------
dreixel's avatar
dreixel committed
344
matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
345
                      -> TcRhoType            -- orig_ty
346
                      -> TcM (TcCoercionN,    -- T k1 k2 k3 a b c ~N orig_ty
dreixel's avatar
dreixel committed
347
                              [TcSigmaType])  -- Element types, k1 k2 k3 a b c
348

349 350 351
-- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
352
-- Postcondition: (T k1 k2 k3 a b c) is well-kinded
353 354

matchExpectedTyConApp tc orig_ty
355
  = go orig_ty
356
  where
357
    go ty
358
       | Just ty' <- coreView ty
359 360
       = go ty'

361
    go ty@(TyConApp tycon args)
362
       | tc == tycon  -- Common case
363
       = return (mkTcNomReflCo ty, args)
364 365 366 367 368 369

    go (TyVarTy tv)
       | ASSERT( isTcTyVar tv) isMetaTyVar tv
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty -> go ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
370
                Flexi       -> defer }
371

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
372
    go _ = defer
373 374 375 376 377 378

    -- If the common case does not occur, instantiate a template
    -- T k1 .. kn t1 .. tm, and unify with the original type
    -- Doing it this way ensures that the types we return are
    -- kind-compatible with T.  For example, suppose we have
    --       matchExpectedTyConApp T (f Maybe)
379 380
    -- where data T a = MkT a
    -- Then we don't want to instantate T's data constructors with
381 382 383
    --    (a::*) ~ Maybe
    -- because that'll make types that are utterly ill-kinded.
    -- This happened in Trac #7368
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
384
    defer
385 386 387 388 389
      = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
           ; traceTc "mtca" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
           ; let args = mkTyVarTys arg_tvs
                 tc_template = mkTyConApp tc args
           ; co <- unifyType noThing tc_template orig_ty
390
           ; return (co, args) }
391

392 393
----------------------
matchExpectedAppTy :: TcRhoType                         -- orig_ty
394
                   -> TcM (TcCoercion,                   -- m a ~N orig_ty
395 396 397
                           (TcSigmaType, TcSigmaType))  -- Returns m, a
-- If the incoming type is a mutable type variable of kind k, then
-- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
Ian Lynagh's avatar
Ian Lynagh committed
398

399 400
matchExpectedAppTy orig_ty
  = go orig_ty
401
  where
402
    go ty
403
      | Just ty' <- coreView ty = go ty'
404

405
      | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
406
      = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
407

408 409 410 411 412
    go (TyVarTy tv)
      | ASSERT( isTcTyVar tv) isMetaTyVar tv
      = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty -> go ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
413
               Flexi       -> defer }
Ian Lynagh's avatar
Ian Lynagh committed
414

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
415
    go _ = defer
Ian Lynagh's avatar
Ian Lynagh committed
416

417
    -- Defer splitting by generating an equality constraint
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
418 419 420
    defer
      = do { ty1 <- newFlexiTyVarTy kind1
           ; ty2 <- newFlexiTyVarTy kind2
421 422
           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
           ; return (co, (ty1, ty2)) }
423

424
    orig_kind = typeKind orig_ty
425
    kind1 = mkFunTy liftedTypeKind orig_kind
426 427
    kind2 = liftedTypeKind    -- m :: * -> k
                              -- arg type :: *
428

Austin Seipp's avatar
Austin Seipp committed
429 430 431
{-
************************************************************************
*                                                                      *
Ian Lynagh's avatar
Ian Lynagh committed
432
                Subsumption checking
Austin Seipp's avatar
Austin Seipp committed
433 434
*                                                                      *
************************************************************************
435

436 437 438 439
Note [Subsumption checking: tcSubType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All the tcSubType calls have the form
                tcSubType actual_ty expected_ty
440
which checks
Ian Lynagh's avatar
Ian Lynagh committed
441
                actual_ty <= expected_ty
442

443
That is, that a value of type actual_ty is acceptable in
444 445 446
a place expecting a value of type expected_ty.  I.e. that

    actual ty   is more polymorphic than   expected_ty
447

Ian Lynagh's avatar
Ian Lynagh committed
448 449
It returns a coercion function
        co_fn :: actual_ty ~ expected_ty
450
which takes an HsExpr of type actual_ty into one of type
451 452
expected_ty.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
These functions do not actually check for subsumption. They check if
expected_ty is an appropriate annotation to use for something of type
actual_ty. This difference matters when thinking about visible type
application. For example,

   forall a. a -> forall b. b -> b
      DOES NOT SUBSUME
   forall a b. a -> b -> b

because the type arguments appear in a different order. (Neither does
it work the other way around.) BUT, these types are appropriate annotations
for one another. Because the user directs annotations, it's OK if some
arguments shuffle around -- after all, it's what the user wants.
Bottom line: none of this changes with visible type application.

468 469 470 471
There are a number of wrinkles (below).

Notice that Wrinkle 1 and 2 both require eta-expansion, which technically
may increase termination.  We just put up with this, in exchange for getting
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
472
more predictable type inference.
473 474 475 476 477 478 479

Wrinkle 1: Note [Deep skolemisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We want   (forall a. Int -> a -> a)  <=  (Int -> forall a. a->a)
(see section 4.6 of "Practical type inference for higher rank types")
So we must deeply-skolemise the RHS before we instantiate the LHS.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
480
That is why tc_sub_type starts with a call to tcSkolemise (which does the
481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
deep skolemisation), and then calls the DS variant (which assumes
that expected_ty is deeply skolemised)

Wrinkle 2: Note [Co/contra-variance of subsumption checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider  g :: (Int -> Int) -> Int
  f1 :: (forall a. a -> a) -> Int
  f1 = g

  f2 :: (forall a. a -> a) -> Int
  f2 x = g x
f2 will typecheck, and it would be odd/fragile if f1 did not.
But f1 will only typecheck if we have that
    (Int->Int) -> Int  <=  (forall a. a->a) -> Int
And that is only true if we do the full co/contravariant thing
in the subsumption check.  That happens in the FunTy case of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
497
tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
HsWrapper.

Another powerful reason for doing this co/contra stuff is visible
in Trac #9569, involving instantiation of constraint variables,
and again involving eta-expansion.

Wrinkle 3: Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider tc150:
  f y = \ (x::forall a. a->a). blah
The following happens:
* We will infer the type of the RHS, ie with a res_ty = alpha.
* Then the lambda will split  alpha := beta -> gamma.
* And then we'll check tcSubType IsSwapped beta (forall a. a->a)

So it's important that we unify beta := forall a. a->a, rather than
skolemising the type.
Austin Seipp's avatar
Austin Seipp committed
515
-}
516

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
517 518 519 520 521 522

-- | Call this variant when you are in a higher-rank situation and
-- you know the right-hand type is deeply skolemised.
tcSubTypeHR :: Outputable a
            => CtOrigin    -- ^ of the actual type
            -> Maybe a     -- ^ If present, it has type ty_actual
523
            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
524 525 526 527
tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt

tcSubType :: Outputable a
          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
528
          -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
529 530
-- Checks that actual <= expected
-- Returns HsWrapper :: actual ~ expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
531
tcSubType ctxt maybe_thing ty_actual ty_expected
532
  = tcSubTypeO origin ctxt ty_actual ty_expected
533 534 535
  where
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
536
                          , uo_thing    = mkErrorThing <$> maybe_thing }
537

538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580

-- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
-- You probably want this only when looking at patterns, never expressions.
tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeET orig ty_actual ty_expected
  = uExpTypeX orig ty_expected ty_actual
              (return . mkWpCastN . mkTcSymCo)
              (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a
                                    (mkCheckExpType ty_expected))

-- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type.
-- You probably want this only when looking at patterns, never expressions.
-- Does not add context.
tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected
  = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual
tcSubTypeET_NC ctxt (Check ty_actual) ty_expected
  = tc_sub_type orig orig ctxt ty_actual ty_expected'
  where
    ty_expected' = mkCheckExpType ty_expected
    orig = TypeEqOrigin { uo_actual   = ty_actual
                        , uo_expected = ty_expected'
                        , uo_thing    = Nothing }

tcSubTypeO :: CtOrigin      -- ^ of the actual type
           -> UserTypeCtxt  -- ^ of the expected type
           -> TcSigmaType
           -> ExpSigmaType
           -> TcM HsWrapper
tcSubTypeO origin ctxt ty_actual ty_expected
  = addSubTypeCtxt ty_actual ty_expected $
    do { traceTc "tcSubType" (vcat [ pprCtOrigin origin
                                   , pprUserTypeCtxt ctxt
                                   , ppr ty_actual
                                   , ppr ty_expected ])
       ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected }
  where
    eq_orig | TypeEqOrigin {} <- origin = origin
            | otherwise
            = TypeEqOrigin { uo_actual   = ty_actual
                           , uo_expected = ty_expected
                           , uo_thing    = Nothing }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
581
tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
582
            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
583 584
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised (hence "DS")
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
585
tcSubTypeDS ctxt m_expr ty_actual ty_expected
586
  = addSubTypeCtxt ty_actual ty_expected $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
587 588 589 590 591 592
    tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected

-- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating
-- the "actual" type
tcSubTypeDS_O :: Outputable a
              => CtOrigin -> UserTypeCtxt
593
              -> Maybe a -> TcSigmaType -> ExpRhoType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
594 595 596 597 598 599 600 601
              -> TcM HsWrapper
tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected
  = addSubTypeCtxt ty_actual ty_expected $
    do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
                                       , pprUserTypeCtxt ctxt
                                       , ppr ty_actual
                                       , ppr ty_expected ])
       ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected }
602

603
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
604
addSubTypeCtxt ty_actual ty_expected thing_inside
605 606 607
 | isRhoTy ty_actual        -- If there is no polymorphism involved, the
 , isRhoExpTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
 = thing_inside             -- gives enough context by itself
608 609 610 611 612
 | otherwise
 = addErrCtxtM mk_msg thing_inside
  where
    mk_msg tidy_env
      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
613 614 615 616 617 618 619
                   -- might not be filled if we're debugging. ugh.
           ; mb_ty_expected          <- readExpType_maybe ty_expected
           ; (tidy_env, ty_expected) <- case mb_ty_expected of
                                          Just ty -> second mkCheckExpType <$>
                                                     zonkTidyTcType tidy_env ty
                                          Nothing -> return (tidy_env, ty_expected)
           ; ty_expected             <- readExpType ty_expected
620
           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
621
           ; let msg = vcat [ hang (text "When checking that:")
622
                                 4 (ppr ty_actual)
623
                            , nest 2 (hang (text "is more polymorphic than:")
624 625 626 627 628 629 630
                                         2 (ppr ty_expected)) ]
           ; return (tidy_env, msg) }

---------------
-- The "_NC" variants do not add a typechecker-error context;
-- the caller is assumed to do that

631
tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
632 633
tcSubType_NC ctxt ty_actual ty_expected
  = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
634
       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
635
  where
636 637 638 639 640 641 642
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
                          , uo_thing    = Nothing }

tcSubTypeDS_NC :: Outputable a
               => UserTypeCtxt
               -> Maybe a  -- ^ If present, this has type ty_actual
643
               -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
644
tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
645
  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
646
       ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
647
  where
648 649 650
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
                          , uo_thing    = mkErrorThing <$> maybe_thing }
651

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
652 653 654 655
tcSubTypeDS_NC_O :: Outputable a
                 => CtOrigin   -- origin used for instantiation only
                 -> UserTypeCtxt
                 -> Maybe a
656
                 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
657 658
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised
659 660 661 662
tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et
  = uExpTypeX eq_orig ty_actual et
      (return . mkWpCastN)
      (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
663
  where
664 665
    eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et
                           , uo_thing = mkErrorThing <$> m_thing }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
666

667
---------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
668 669
tc_sub_type :: CtOrigin   -- origin used when calling uType
            -> CtOrigin   -- origin used when instantiating
670 671 672 673 674 675 676 677 678 679
            -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper
tc_sub_type eq_orig inst_orig ctxt ty_actual et
  = uExpTypeX eq_orig ty_actual et
      (return . mkWpCastN)
      (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual)

tc_sub_tc_type :: CtOrigin   -- used when calling uType
               -> CtOrigin   -- used when instantiating
               -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
680 681 682
  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
  = do { lookup_res <- lookupTcTyVar tv_actual
       ; case lookup_res of
683 684
           Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig
                                               ctxt ty_actual' ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
685 686 687 688 689 690 691 692 693 694

             -- It's tempting to see if tv_actual can unify with a polytype
             -- and, if so, call uType; otherwise, skolemise first. But this
             -- is wrong, because skolemising will bump the TcLevel and the
             -- unification will fail anyway.
             -- It's also tempting to call uUnfilledVar directly, but calling
             -- uType seems safer in the presence of possible refactoring
             -- later.
           Unfilled _        -> mkWpCastN <$>
                                uType eq_orig TypeLevel ty_actual ty_expected }
695 696

  | otherwise  -- See Note [Deep skolemisation]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
697 698 699 700
  = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
                                  \ _ sk_rho ->
                                  tc_sub_type_ds eq_orig inst_orig ctxt
                                                 ty_actual sk_rho
701 702 703
       ; return (sk_wrap <.> inner_wrap) }

---------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
704 705 706
tc_sub_type_ds :: CtOrigin    -- used when calling uType
               -> CtOrigin    -- used when instantiating
               -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
707 708
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
709 710 711 712 713 714 715 716 717 718 719 720 721
tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
  = go ty_actual ty_expected
  where
    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'

    go (TyVarTy tv_a) ty_e
      = do { lookup_res <- lookupTcTyVar tv_a
           ; case lookup_res of
               Filled ty_a' ->
                 do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:"
                        (ppr tv_a <+> text "-->" <+> ppr ty_a')
                    ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
722
               Unfilled _   -> unify }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
723

724 725 726 727 728 729 730
    -- Historical note (Sept 16): there was a case here for
    --    go ty_a (TyVarTy alpha)
    -- which, in the impredicative case unified  alpha := ty_a
    -- where th_a is a polytype.  Not only is this probably bogus (we
    -- simply do not have decent story for imprdicative types), but it
    -- caused Trac #12616 because (also bizarrely) 'deriving' code had
    -- -XImpredicativeTypes on.  I deleted the entire case.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
731

Simon Peyton Jones's avatar
Simon Peyton Jones committed
732
    go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
733 734 735 736 737
      | not (isPredTy act_arg)
      , not (isPredTy exp_arg)
      = -- See Note [Co/contra-variance of subsumption checking]
        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res
           ; arg_wrap
738
               <- tc_sub_tc_type eq_orig (GivenOrigin
739
                                          (SigSkol GenSigCtxt exp_arg))
740
                                 ctxt exp_arg act_arg
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
741 742 743 744 745 746 747 748
           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) }
               -- arg_wrap :: exp_arg ~ act_arg
               -- res_wrap :: act-res ~ exp_res

    go ty_a ty_e
      | let (tvs, theta, _) = tcSplitSigmaTy ty_a
      , not (null tvs && null theta)
      = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
749 750 751 752 753
           ; body_wrap <- tc_sub_type_ds
                            (eq_orig { uo_actual = in_rho
                                     , uo_expected =
                                         mkCheckExpType ty_expected })
                            inst_orig ctxt in_rho ty_e
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
754 755 756
           ; return (body_wrap <.> in_wrap) }

      | otherwise   -- Revert to unification
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
757 758 759
      = inst_and_unify
         -- It's still possible that ty_actual has nested foralls. Instantiate
         -- these, as there's no way unification will succeed with them in.
760 761 762 763
         -- See typecheck/should_compile/T11305 for an example of when this
         -- is important. The problem is that we're checking something like
         --  a -> forall b. b -> b     <=   alpha beta gamma
         -- where we end up with alpha := (->)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
764 765 766 767 768 769 770 771 772

    inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual

                           -- if we haven't recurred through an arrow, then
                           -- the eq_orig will list ty_actual. In this case,
                           -- we want to update the origin to reflect the
                           -- instantiation. If we *have* recurred through
                           -- an arrow, it's better not to update.
                        ; let eq_orig' = case eq_orig of
773
                                TypeEqOrigin { uo_actual   = orig_ty_actual }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
774 775
                                  |  orig_ty_actual `tcEqType` ty_actual
                                  ,  not (isIdHsWrapper wrap)
776
                                  -> eq_orig { uo_actual = rho_a }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
777 778 779 780 781
                                _ -> eq_orig

                        ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
                        ; return (mkWpCastN cow <.> wrap) }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
782 783

     -- use versions without synonyms expanded
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
784
    unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected
785

786
-----------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
787 788
-- needs both un-type-checked (for origins) and type-checked (for wrapping)
-- expressions
789
tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> ExpRhoType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
790 791 792 793 794
             -> TcM (HsExpr TcId)
tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr)

-- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
-- convenient.
795
tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> ExpRhoType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
796 797 798 799 800 801
               -> TcM (HsExpr TcId)
tcWrapResultO orig expr actual_ty res_ty
  = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                      , text "Expected:" <+> ppr res_ty ])
       ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
                                 (Just expr) actual_ty res_ty
802
       ; return (mkHsWrap cow expr) }
803 804

-----------------------------------
Ian Lynagh's avatar
Ian Lynagh committed
805
wrapFunResCoercion
806 807 808
        :: [TcType]        -- Type of args
        -> HsWrapper       -- HsExpr a -> HsExpr b
        -> TcM HsWrapper   -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
809
wrapFunResCoercion arg_tys co_fn_res
Ian Lynagh's avatar
Ian Lynagh committed
810
  | isIdHsWrapper co_fn_res
811
  = return idHsWrapper
Ian Lynagh's avatar
Ian Lynagh committed
812
  | null arg_tys
813
  = return co_fn_res
814
  | otherwise
Ian Lynagh's avatar
Ian Lynagh committed
815
  = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
816
        ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
817

818
-----------------------------------
819 820 821
-- | Infer a type using a fresh ExpType
-- See also Note [ExpType] in TcMType
tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType)
822
tcInfer tc_check
823 824 825 826
  = do { res_ty <- newOpenInferExpType
       ; result <- tc_check res_ty
       ; res_ty <- readExpType res_ty
       ; return (result, res_ty) }
827

Austin Seipp's avatar
Austin Seipp committed
828 829 830
{-
************************************************************************
*                                                                      *
831
\subsection{Generalisation}
Austin Seipp's avatar
Austin Seipp committed
832 833 834
*                                                                      *
************************************************************************
-}
835

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
836 837 838 839 840
-- | Take an "expected type" and strip off quantifiers to expose the
-- type underneath, binding the new skolems for the @thing_inside@.
-- The returned 'HsWrapper' has type @specific_ty -> expected_ty@.
tcSkolemise :: UserTypeCtxt -> TcSigmaType
            -> ([TcTyVar] -> TcType -> TcM result)
841
         -- ^ These are only ever used for scoped type variables.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
842 843
            -> TcM (HsWrapper, result)
        -- ^ The expression has type: spec_ty -> expected_ty
Ian Lynagh's avatar
Ian Lynagh committed
844

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
845
tcSkolemise ctxt expected_ty thing_inside
846 847
   -- We expect expected_ty to be a forall-type
   -- If not, the call is a no-op
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
848
  = do  { traceTc "tcSkolemise" Outputable.empty
849
        ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
850

851
        ; lvl <- getTcLevel
Ian Lynagh's avatar
Ian Lynagh committed
852
        ; when debugIsOn $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
853
              traceTc "tcSkolemise" $ vcat [
854 855 856 857 858
                ppr lvl,
                text "expected_ty" <+> ppr expected_ty,
                text "inst tyvars" <+> ppr tvs',
                text "given"       <+> ppr given,
                text "inst type"   <+> ppr rho' ]
859

860
        -- Generally we must check that the "forall_tvs" havn't been constrained
Ian Lynagh's avatar
Ian Lynagh committed
861 862 863 864 865 866 867
        -- 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.
868 869
        --
        -- However [Oct 10] now that the untouchables are a range of
870
        -- TcTyVars, all this is handled automatically with no need for
871
        -- extra faffing around
872

873 874
        -- Use the *instantiated* type in the SkolemInfo
        -- so that the names of displayed type variables line up
875
        ; let skol_info = SigSkol ctxt (mkFunTys (map varType given) rho')
876

877
        ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
878 879 880
                                thing_inside tvs' rho'

        ; return (wrap <.> mkWpLet ev_binds, result) }
881 882
          -- The ev_binds returned by checkConstraints is very
          -- often empty, in which case mkWpLet is a no-op
883

884 885 886 887 888 889 890 891 892
-- | Variant of 'tcSkolemise' that takes an ExpType
tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
              -> (ExpRhoType -> TcM result)
              -> TcM (HsWrapper, result)
tcSkolemiseET _ et@(Infer {}) thing_inside
  = (idHsWrapper, ) <$> thing_inside et
tcSkolemiseET ctxt (Check ty) thing_inside
  = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType

893
checkConstraints :: SkolemInfo
894 895 896 897
                 -> [TcTyVar]           -- Skolems
                 -> [EvVar]             -- Given
                 -> TcM result
                 -> TcM (TcEvBinds, result)
898

899
checkConstraints skol_info skol_tvs given thing_inside
900 901
  = do { (implics, ev_binds, result)
            <- buildImplication skol_info skol_tvs given thing_inside
902 903 904 905 906 907 908 909 910
       ; emitImplications implics
       ; return (ev_binds, result) }

buildImplication :: SkolemInfo
                 -> [TcTyVar]           -- Skolems
                 -> [EvVar]             -- Given
                 -> TcM result
                 -> TcM (Bag Implication, TcEvBinds, result)
buildImplication skol_info skol_tvs given thing_inside
911 912 913 914 915 916 917
  = do { tc_lvl <- getTcLevel
       ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||>
                                 goptM Opt_DeferTypedHoles
       ; if null skol_tvs && null given && (not deferred_type_errors ||
                                            not (isTopTcLevel tc_lvl))
         then do { res <- thing_inside
                 ; return (emptyBag, emptyTcEvBinds, res) }
918
      -- Fast path.  We check every function argument with
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
919
      -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
920 921 922
      -- But with the solver producing unlifted equalities, we need
      -- to have an EvBindsVar for them when they might be deferred to
      -- runtime. Otherwise, they end up as top-level unlifted bindings,
923 924
      -- which are verboten. See also Note [Deferred errors for coercion holes]
      -- in TcErrors.
925 926
         else
    do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
927
       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
928
       ; return (implics, ev_binds, result) }}
929 930 931 932 933 934 935 936 937 938 939 940 941 942

buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
                   -> [EvVar] -> WantedConstraints
                   -> TcM (Bag Implication, TcEvBinds)
buildImplicationFor tclvl skol_info skol_tvs given wanted
  | isEmptyWC wanted && null given
             -- Optimisation : if there are no wanteds, and no givens
             -- don't generate an implication at all.
             -- Reason for the (null given): we don't want to lose
             -- the "inaccessible alternative" error check
  = return (emptyBag, emptyTcEvBinds)

  | otherwise
  = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
943
    ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
944
    do { ev_binds_var <- newTcEvBinds
945
       ; env <- getLclEnv
946 947 948 949 950 951
       ; let implic = Implic { ic_tclvl = tclvl
                             , ic_skols = skol_tvs
                             , ic_no_eqs = False
                             , ic_given = given
                             , ic_wanted = wanted
                             , ic_status  = IC_Unsolved
952
                             , ic_binds = Just ev_binds_var
953 954 955
                             , ic_env = env
                             , ic_info = skol_info }

956
       ; return (unitBag implic, TcEvBinds ev_binds_var) }
957

Austin Seipp's avatar
Austin Seipp committed
958 959 960
{-
************************************************************************
*                                                                      *
Ian Lynagh's avatar
Ian Lynagh committed
961
                Boxy unification
Austin Seipp's avatar
Austin Seipp committed
962 963
*                                                                      *
************************************************************************
964 965 966

The exported functions are all defined as versions of some
non-exported generic functions.
Austin Seipp's avatar
Austin Seipp committed
967
-}
968

969
unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
970
          -> TcTauType -> TcTauType -> TcM TcCoercionN
971 972
-- Actual and expected types
-- Returns a coercion : ty1 ~ ty2
973
unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2