TcUnify.hs 63.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
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
13 14 15
  tcWrapResult, tcWrapResultO, tcSkolemise,
  tcSubTypeHR, tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O,
  tcSubTypeDS_NC, tcSubTypeDS_NC_O,
16
  checkConstraints, buildImplication, buildImplicationFor,
17

dreixel's avatar
dreixel committed
18
  -- Various unifications
19 20
  unifyType_, unifyType, unifyTheta, unifyKind, noThing,
  uType,
21

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

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

35 36 37 38
  ) where

#include "HsVersions.h"

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

import Control.Monad
64

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

72 73 74 75 76 77 78
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"
79

80
This is used to construct a message of form
81

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

94 95
Note [matchExpectedFunTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
96
matchExpectedFunTys checks that a sigma has the form
97 98 99 100 101
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:
102 103
        A lambda expression
        A function definition
104 105
     An operator section

Austin Seipp's avatar
Austin Seipp committed
106
-}
107

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
108 109
-- Use this one when you have an "expected" type.
matchExpectedFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
110
                    -> Arity
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 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
                    -> TcSigmaType  -- deeply skolemised
                    -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
-- If    matchExpectedFunTys n ty = (wrap, [t1,..,tn], ty_r)
-- then  wrap : (t1 -> ... -> tn -> ty_r) "->" ty

-- This function is always called with a deeply skolemised expected result
-- type. This means that matchActualFunTys will never actually instantiate,
-- and the returned HsWrapper will be reversible (that is, just a coercion).
-- So we just piggyback on matchActualFunTys. This is just a bit dodgy, but
-- it's much better than duplicating all the logic in matchActualFunTys.
-- To keep expected/actual working out properly, we tell matchActualFunTys
-- to swap the arguments to unifyType.
matchExpectedFunTys herald arity ty
  = ASSERT( is_deeply_skolemised ty )
    do { (wrap, arg_tys, res_ty)
           <- match_fun_tys True herald
                            (Shouldn'tHappenOrigin "matchExpectedFunTys")
                            arity ty [] arity
       ; return $
         case symWrapper_maybe wrap of
           Just wrap' -> (wrap', arg_tys, res_ty)
           Nothing    -> pprPanic "matchExpectedFunTys" (ppr wrap $$ ppr ty) }
  where
    is_deeply_skolemised (TyVarTy {})    = True
    is_deeply_skolemised (AppTy {})      = True
    is_deeply_skolemised (TyConApp {})   = True
    is_deeply_skolemised (LitTy {})      = True
    is_deeply_skolemised (CastTy ty _)   = is_deeply_skolemised ty
    is_deeply_skolemised (CoercionTy {}) = True

    is_deeply_skolemised (ForAllTy (Anon _) res) = is_deeply_skolemised res
    is_deeply_skolemised (ForAllTy (Named {}) _) = False

matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
                  -> CtOrigin
                  -> Arity
                  -> TcSigmaType
                  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
matchActualFunTys herald ct_orig arity ty
  = matchActualFunTysPart herald ct_orig arity ty [] arity

-- | Variant of 'matchActualFunTys' that works when supplied only part
-- (that is, to the right of some arrows) of the full function type
matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
                      -> CtOrigin
                      -> Arity
                      -> TcSigmaType
                      -> [TcSigmaType] -- reversed args. See (*) below.
                      -> Arity   -- overall arity of the function, for errs
                      -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
matchActualFunTysPart = match_fun_tys False

match_fun_tys :: Bool -- True <=> swap the args when unifying,
                      -- for better expected/actual in error messages;
                      -- see comments with matchExpectedFunTys
              -> SDoc
              -> CtOrigin
              -> Arity
              -> TcSigmaType
              -> [TcSigmaType]
              -> Arity
              -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
match_fun_tys swap_tys herald ct_orig arity orig_ty orig_old_args full_arity
  = go arity orig_old_args orig_ty
-- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
-- then  wrap : ty "->" (t1 -> ... -> tn -> ty_r)
177
--
178 179
-- Does not allocate unnecessary meta variables: if the input already is
-- a function, we just take it apart.  Not only is this efficient,
180
-- it's important for higher rank: the argument might be of form
181
--              (forall a. ty) -> other
182 183 184
-- 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
185 186 187 188 189
-- (*) 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).
190

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
  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
217

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
218 219
    go n acc_args ty
      | Just ty' <- coreView ty = go n acc_args ty'
220

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
221 222 223 224 225
    go n acc_args (ForAllTy (Anon arg_ty) res_ty)
      = ASSERT( not (isPredTy arg_ty) )
        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
           ; return ( mkWpFun idHsWrapper wrap_res arg_ty (mkFunTys tys ty_r)
                    , arg_ty:tys, ty_r ) }
226

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
227
    go n acc_args ty@(TyVarTy tv)
228 229
      | ASSERT( isTcTyVar tv) isMetaTyVar tv
      = do { cts <- readMetaTyVar tv
230
           ; case cts of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
231 232
               Indirect ty' -> go n acc_args ty'
               Flexi        -> defer n ty (isReturnTyVar tv) }
233 234

       -- In all other cases we bale out into ordinary unification
235
       -- However unlike the meta-tyvar case, we are sure that the
236 237 238 239 240 241 242 243 244 245 246 247 248
       -- 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
249 250
    go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
                       defer n ty False
251 252

    ------------
253
    -- If we decide that a ReturnTv (see Note [ReturnTv] in TcType) should
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
254 255 256 257
    -- really be a function type, then we need to allow the
    -- result types also to be a ReturnTv.
    defer n fun_ty is_return
      = do { arg_tys <- replicateM n new_flexi
258
           ; res_ty  <- new_flexi
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
259 260 261 262 263
           ; let unif_fun_ty = mkFunTys arg_tys res_ty
           ; co <- if swap_tys
                   then mkTcSymCo <$> unifyType noThing unif_fun_ty fun_ty
                   else               unifyType noThing fun_ty unif_fun_ty
           ; return (mkWpCastN co, arg_tys, res_ty) }
264
      where
265 266 267 268
        -- preserve ReturnTv-ness
        new_flexi :: TcM TcType
        new_flexi | is_return = (mkTyVarTy . fst) <$> newOpenReturnTyVar
                  | otherwise = newOpenFlexiTyVarTy
269 270

    ------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
271 272 273 274 275 276 277 278 279 280 281 282 283 284
    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
           ; return (env2, mk_msg unzonked zonked n_actual) }

    mk_msg full_ty ty n_args
      = herald <+> speakNOf full_arity (text "argument") <> comma $$
        if n_args == full_arity
          then ptext (sLit "its type is") <+> quotes (pprType full_ty) <>
285 286 287 288 289
               comma $$
               ptext (sLit "it is specialized to") <+> quotes (pprType ty)
          else sep [ptext (sLit "but its type") <+> quotes (pprType ty),
                    if n_args == 0 then ptext (sLit "has none")
                    else ptext (sLit "has only") <+> speakN n_args]
290

291
----------------------
292
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
293
-- Special case for lists
294
matchExpectedListTy exp_ty
batterseapower's avatar
batterseapower committed
295 296
 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
      ; return (co, elt_ty) }
297

298
----------------------
299
matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
300
-- Special case for parrs
301
matchExpectedPArrTy exp_ty
batterseapower's avatar
batterseapower committed
302 303
  = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
       ; return (co, elt_ty) }
304

305
---------------------
dreixel's avatar
dreixel committed
306
matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
307
                      -> TcRhoType            -- orig_ty
308
                      -> TcM (TcCoercionN,    -- T k1 k2 k3 a b c ~N orig_ty
dreixel's avatar
dreixel committed
309
                              [TcSigmaType])  -- Element types, k1 k2 k3 a b c
310

311 312 313
-- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
314
-- Postcondition: (T k1 k2 k3 a b c) is well-kinded
315 316

matchExpectedTyConApp tc orig_ty
317
  = go orig_ty
318
  where
319
    go ty
320
       | Just ty' <- coreView ty
321 322
       = go ty'

323
    go ty@(TyConApp tycon args)
324
       | tc == tycon  -- Common case
325
       = return (mkTcNomReflCo ty, args)
326 327 328 329 330 331

    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
332
                Flexi       -> defer }
333

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
334
    go _ = defer
335 336 337 338 339 340

    -- 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)
341 342
    -- where data T a = MkT a
    -- Then we don't want to instantate T's data constructors with
343 344 345
    --    (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
346
    defer
347
      = ASSERT2( classifiesTypeWithValues res_kind, ppr tc )
348
        do { (k_subst, kvs') <- newMetaTyVars kvs
349 350
           ; let arg_kinds' = substTys k_subst arg_kinds
                 kappa_tys  = mkTyVarTys kvs'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
351
           ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
352 353 354 355 356
           ; co <- unifyType noThing (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty
           ; return (co, kappa_tys ++ tau_tys) }

    (bndrs, res_kind)     = splitPiTys (tyConKind tc)
    (kvs, arg_kinds)      = partitionBinders bndrs
357

358 359
----------------------
matchExpectedAppTy :: TcRhoType                         -- orig_ty
360
                   -> TcM (TcCoercion,                   -- m a ~N orig_ty
361 362 363
                           (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
364

365 366
matchExpectedAppTy orig_ty
  = go orig_ty
367
  where
368
    go ty
369
      | Just ty' <- coreView ty = go ty'
370

371
      | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
372
      = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
373

374 375 376 377 378
    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
379
               Flexi       -> defer }
Ian Lynagh's avatar
Ian Lynagh committed
380

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

383
    -- Defer splitting by generating an equality constraint
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
384 385 386
    defer
      = do { ty1 <- newFlexiTyVarTy kind1
           ; ty2 <- newFlexiTyVarTy kind2
387 388
           ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty
           ; return (co, (ty1, ty2)) }
389

390
    orig_kind = typeKind orig_ty
391
    kind1 = mkFunTy liftedTypeKind orig_kind
392 393
    kind2 = liftedTypeKind    -- m :: * -> k
                              -- arg type :: *
394

Austin Seipp's avatar
Austin Seipp committed
395 396 397
{-
************************************************************************
*                                                                      *
Ian Lynagh's avatar
Ian Lynagh committed
398
                Subsumption checking
Austin Seipp's avatar
Austin Seipp committed
399 400
*                                                                      *
************************************************************************
401

402 403 404 405
Note [Subsumption checking: tcSubType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All the tcSubType calls have the form
                tcSubType actual_ty expected_ty
406
which checks
Ian Lynagh's avatar
Ian Lynagh committed
407
                actual_ty <= expected_ty
408

409
That is, that a value of type actual_ty is acceptable in
410 411 412
a place expecting a value of type expected_ty.  I.e. that

    actual ty   is more polymorphic than   expected_ty
413

Ian Lynagh's avatar
Ian Lynagh committed
414 415
It returns a coercion function
        co_fn :: actual_ty ~ expected_ty
416
which takes an HsExpr of type actual_ty into one of type
417 418
expected_ty.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
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.

434 435 436 437
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
438
more predictable type inference.
439 440 441 442 443 444 445

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
446
That is why tc_sub_type starts with a call to tcSkolemise (which does the
447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462
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
463
tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480
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
481
-}
482

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
483 484 485 486 487 488 489 490 491 492 493

-- | 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
            -> TcSigmaType -> TcRhoType -> TcM HsWrapper
tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt

tcSubType :: Outputable a
          => UserTypeCtxt -> Maybe a  -- ^ If present, it has type ty_actual
494
          -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
495 496
-- Checks that actual <= expected
-- Returns HsWrapper :: actual ~ expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
497
tcSubType ctxt maybe_thing ty_actual ty_expected
498
  = addSubTypeCtxt ty_actual ty_expected $
499
    do { traceTc "tcSubType" (vcat [ pprUserTypeCtxt ctxt
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
500
                                   , ppr maybe_thing
501 502
                                   , ppr ty_actual
                                   , ppr ty_expected ])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
503
       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
504 505 506
  where
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
507
                          , uo_thing    = mkErrorThing <$> maybe_thing }
508

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
509
tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a  -- ^ has type ty_actual
510
            -> TcSigmaType -> TcRhoType -> TcM HsWrapper
511 512
-- 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
513
tcSubTypeDS ctxt m_expr ty_actual ty_expected
514
  = addSubTypeCtxt ty_actual ty_expected $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
    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
              -> Maybe a -> TcSigmaType -> TcRhoType
              -> 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 }
530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554

addSubTypeCtxt :: TcType -> TcType -> TcM a -> TcM a
addSubTypeCtxt ty_actual ty_expected thing_inside
 | isRhoTy ty_actual     -- If there is no polymorphism involved, the
 , isRhoTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
 = thing_inside          -- gives enough context by itself
 | otherwise
 = addErrCtxtM mk_msg thing_inside
  where
    mk_msg tidy_env
      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
           ; let msg = vcat [ hang (ptext (sLit "When checking that:"))
                                 4 (ppr ty_actual)
                            , nest 2 (hang (ptext (sLit "is more polymorphic than:"))
                                         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

tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
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
555
       ; tc_sub_type origin origin ctxt ty_actual ty_expected }
556
  where
557 558 559 560 561 562 563 564 565
    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
               -> TcSigmaType -> TcRhoType -> TcM HsWrapper
tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected
566
  = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
567
       ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected }
568
  where
569 570 571
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
                          , uo_thing    = mkErrorThing <$> maybe_thing }
572

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
573 574 575 576 577 578 579 580 581 582 583 584 585
tcSubTypeDS_NC_O :: Outputable a
                 => CtOrigin   -- origin used for instantiation only
                 -> UserTypeCtxt
                 -> Maybe a
                 -> TcSigmaType -> TcRhoType -> TcM HsWrapper
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised
tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
  = tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
  where
    eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected
                           , uo_thing = mkErrorThing <$> m_thing}

586
---------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
tc_sub_type :: CtOrigin   -- origin used when calling uType
            -> CtOrigin   -- origin used when instantiating
            -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tc_sub_type eq_orig inst_orig ctxt ty_actual ty_expected
  | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types]
  = do { lookup_res <- lookupTcTyVar tv_actual
       ; case lookup_res of
           Filled ty_actual' -> tc_sub_type eq_orig inst_orig
                                            ctxt ty_actual' ty_expected

             -- 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 }
606 607

  | otherwise  -- See Note [Deep skolemisation]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
608 609 610 611
  = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
                                  \ _ sk_rho ->
                                  tc_sub_type_ds eq_orig inst_orig ctxt
                                                 ty_actual sk_rho
612 613 614
       ; return (sk_wrap <.> inner_wrap) }

---------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
615 616 617
tc_sub_type_ds :: CtOrigin    -- used when calling uType
               -> CtOrigin    -- used when instantiating
               -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
618 619
-- 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
620 621 622 623 624 625 626 627 628 629 630 631 632
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
633
               Unfilled _   -> unify }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
634 635 636 637 638 639 640 641 642 643 644 645 646 647


    go ty_a (TyVarTy tv_e)
      = do { dflags <- getDynFlags
           ; tclvl  <- getTcLevel
           ; lookup_res <- lookupTcTyVar tv_e
           ; case lookup_res of
               Filled ty_e' ->
                 do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:"
                        (ppr tv_e <+> text "-->" <+> ppr ty_e')
                    ; tc_sub_type eq_orig inst_orig ctxt ty_a ty_e' }
               Unfilled details
                 |  canUnifyWithPolyType dflags details
                    && isTouchableMetaTyVar tclvl tv_e  -- don't want skolems here
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
648
                 -> unify
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
649 650 651 652 653 654

     -- We've avoided instantiating ty_actual just in case ty_expected is
     -- polymorphic. But we've now assiduously determined that it is *not*
     -- polymorphic. So instantiate away. This is needed for e.g. test
     -- typecheck/should_compile/T4284.
                 |  otherwise
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
655
                 -> inst_and_unify }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676

    go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
      | 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
               <- tc_sub_type eq_orig (GivenOrigin (SigSkol GenSigCtxt exp_arg))
                              ctxt exp_arg act_arg
           ; 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
           ; body_wrap <- tcSubTypeDS_NC_O inst_orig ctxt noThing in_rho ty_e
           ; return (body_wrap <.> in_wrap) }

      | otherwise   -- Revert to unification
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
677 678 679
      = 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.
680 681 682 683
         -- 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
684 685 686 687 688 689 690 691 692

    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
693
                                TypeEqOrigin { uo_actual   = orig_ty_actual }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
694 695
                                  |  orig_ty_actual `tcEqType` ty_actual
                                  ,  not (isIdHsWrapper wrap)
696
                                  -> eq_orig { uo_actual = rho_a }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
697 698 699 700 701
                                _ -> 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
702 703

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

706
-----------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
-- needs both un-type-checked (for origins) and type-checked (for wrapping)
-- expressions
tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> TcRhoType
             -> 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.
tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> TcRhoType
               -> 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
722
       ; return (mkHsWrap cow expr) }
723 724

-----------------------------------
Ian Lynagh's avatar
Ian Lynagh committed
725
wrapFunResCoercion
726 727 728
        :: [TcType]        -- Type of args
        -> HsWrapper       -- HsExpr a -> HsExpr b
        -> TcM HsWrapper   -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b)
729
wrapFunResCoercion arg_tys co_fn_res
Ian Lynagh's avatar
Ian Lynagh committed
730
  | isIdHsWrapper co_fn_res
731
  = return idHsWrapper
Ian Lynagh's avatar
Ian Lynagh committed
732
  | null arg_tys
733
  = return co_fn_res
734
  | otherwise
Ian Lynagh's avatar
Ian Lynagh committed
735
  = do  { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys
736
        ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) }
737

738 739 740 741 742
-----------------------------------
-- | Infer a type using a type "checking" function by passing in a ReturnTv,
-- which can unify with *anything*. See also Note [ReturnTv] in TcType
tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
tcInfer tc_check
743
  = do { (ret_tv, ret_kind) <- newOpenReturnTyVar
744 745 746 747 748 749
       ; res <- tc_check (mkTyVarTy ret_tv)
       ; details <- readMetaTyVar ret_tv
       ; res_ty <- case details of
            Indirect ty -> return ty
            Flexi ->    -- Checking was uninformative
                     do { traceTc "Defaulting un-filled ReturnTv to a TauTv" (ppr ret_tv)
750
                        ; tau_ty <- newFlexiTyVarTy ret_kind
751 752 753
                        ; writeMetaTyVar ret_tv tau_ty
                        ; return tau_ty }
       ; return (res, res_ty) }
754

Austin Seipp's avatar
Austin Seipp committed
755 756 757
{-
************************************************************************
*                                                                      *
758
\subsection{Generalisation}
Austin Seipp's avatar
Austin Seipp committed
759 760 761
*                                                                      *
************************************************************************
-}
762

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
763 764 765 766 767
-- | 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)
768 769 770
         -- ^ thing_inside is passed only the *type* variables, not
         -- *coercion* variables. They are only ever used for scoped type
         -- variables.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
771 772
            -> TcM (HsWrapper, result)
        -- ^ The expression has type: spec_ty -> expected_ty
Ian Lynagh's avatar
Ian Lynagh committed
773

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
774
tcSkolemise ctxt expected_ty thing_inside
775 776
   -- 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
777
  = do  { traceTc "tcSkolemise" Outputable.empty
778
        ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty
779

780
        ; lvl <- getTcLevel
Ian Lynagh's avatar
Ian Lynagh committed
781
        ; when debugIsOn $
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
782
              traceTc "tcSkolemise" $ vcat [
783 784 785 786 787
                ppr lvl,
                text "expected_ty" <+> ppr expected_ty,
                text "inst tyvars" <+> ppr tvs',
                text "given"       <+> ppr given,
                text "inst type"   <+> ppr rho' ]
788

789
        -- Generally we must check that the "forall_tvs" havn't been constrained
Ian Lynagh's avatar
Ian Lynagh committed
790 791 792 793 794 795 796
        -- 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.
797 798
        --
        -- However [Oct 10] now that the untouchables are a range of
799
        -- TcTyVars, all this is handled automatically with no need for
800
        -- extra faffing around
801

802 803
        -- Use the *instantiated* type in the SkolemInfo
        -- so that the names of displayed type variables line up
804
        ; let skol_info = SigSkol ctxt (mkFunTys (map varType given) rho')
805

806
        ; (ev_binds, result) <- checkConstraints skol_info tvs' given $
807 808 809
                                thing_inside tvs' rho'

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

checkConstraints :: SkolemInfo
814 815 816 817
                 -> [TcTyVar]           -- Skolems
                 -> [EvVar]             -- Given
                 -> TcM result
                 -> TcM (TcEvBinds, result)
818

819
checkConstraints skol_info skol_tvs given thing_inside
820 821
  = do { (implics, ev_binds, result)
            <- buildImplication skol_info skol_tvs given thing_inside
822 823 824 825 826 827 828 829 830
       ; 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
831 832 833 834 835 836 837
  = 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) }
838
      -- Fast path.  We check every function argument with
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
839
      -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints.
840 841 842
      -- 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,
843 844
      -- which are verboten. See also Note [Deferred errors for coercion holes]
      -- in TcErrors.
845 846
         else
    do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
847
       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
848
       ; return (implics, ev_binds, result) }}
849 850 851 852 853 854 855 856 857 858 859 860 861 862

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 )
863
    ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
864
    do { ev_binds_var <- newTcEvBinds
865
       ; env <- getLclEnv
866 867 868 869 870 871
       ; let implic = Implic { ic_tclvl = tclvl
                             , ic_skols = skol_tvs
                             , ic_no_eqs = False
                             , ic_given = given
                             , ic_wanted = wanted
                             , ic_status  = IC_Unsolved
872
                             , ic_binds = Just ev_binds_var
873 874 875
                             , ic_env = env
                             , ic_info = skol_info }

876
       ; return (unitBag implic, TcEvBinds ev_binds_var) }
877

Austin Seipp's avatar
Austin Seipp committed
878 879 880
{-
************************************************************************
*                                                                      *
Ian Lynagh's avatar
Ian Lynagh committed
881
                Boxy unification
Austin Seipp's avatar
Austin Seipp committed
882 883
*                                                                      *
************************************************************************
884 885 886

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

889 890 891 892 893 894 895 896
-- | Unify two types, discarding a resultant coercion. Any constraints
-- generated will still need to be solved, however.
unifyType_ :: Outputable a => Maybe a  -- ^ If present, has type 'ty1'
           -> TcTauType -> TcTauType -> TcM ()
unifyType_ thing ty1 ty2 = void $ unifyType thing ty1 ty2

unifyType :: Outputable a => Maybe a   -- ^ If present, has type 'ty1'
          -> TcTauType -> TcTauType -> TcM TcCoercion
897 898
-- Actual and expected types
-- Returns a coercion : ty1 ~ ty2
899
unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2
900
  where
901 902 903 904 905 906 907 908 909 910 911 912 913
    origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
                          , uo_thing  = mkErrorThing <$> thing }

-- | Use this instead of 'Nothing' when calling 'unifyType' without
-- a good "thing" (where the "thing" has the "actual" type passed in)
-- This has an 'Outputable' instance, avoiding amgiguity problems.
noThing :: Maybe (HsExpr Name)
noThing = Nothing

unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM Coercion
unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2
  where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2
                              , uo_thing  = mkErrorThing <$> thing }
914 915

---------------
916
unifyPred :: PredType -> PredType -> TcM TcCoercion
917
-- Actual and expected types
918
unifyPred = unifyType noThing
919

920
---------------
921
unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion]
922
-- Actual and expected types
923
unifyTheta theta1 theta2
Ian Lynagh's avatar
Ian Lynagh committed
924 925
  = do  { checkTc (equalLength theta1 theta2)
                  (vcat [ptext (sLit "Contexts differ in length"),
926
                         nest 2 $ parens $ ptext (sLit "Use RelaxedPolyRec to allow this")])
927
        ; zipWithM unifyPred theta1 theta2 }
928

Austin Seipp's avatar
Austin Seipp committed
929
{-
930 931
%************************************************************************
%*                                                                      *
932
                 uType and friends
933 934
%*                                                                      *
%************************************************************************
935

936
uType is the heart of the unifier.
Austin Seipp's avatar
Austin Seipp committed
937
-}
938

939
------------
940 941
uType, uType_defer
  :: CtOrigin
942
  -> TypeOrKind
943 944
  -> TcType    -- ty1 is the *actual* type
  -> TcType    -- ty2 is the *expected* type
945
  -> TcM Coercion
946 947

--------------
948 949
-- It is always safe to defer unification to the main constraint solver
-- See Note [Deferred unification]
950 951 952
uType_defer origin t_or_k ty1 ty2
  = do { hole <- newCoercionHole
       ; loc <- getCtLocM origin (Just t_or_k)
953
       ; emitSimple $ mkNonCanonical $
954 955
             CtWanted { ctev_dest = HoleDest hole
                      , ctev_pred = mkPrimEqPred ty1 ty2
956
                      , ctev_loc = loc }
957 958

       -- Error trace only