TcUnify.hs 88.8 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

9
{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

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

dreixel's avatar
dreixel committed
19
  -- Various unifications
20
  unifyType, unifyKind,
21
  uType, promoteTcType,
22
  swapOverTyVars, canSolveByUnification,
23

24 25
  --------------------------------
  -- Holes
26
  tcInferInst, tcInferNoInst,
batterseapower's avatar
batterseapower committed
27 28
  matchExpectedListTy,
  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

34
  metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
dreixel's avatar
dreixel committed
35

36 37 38 39
  ) where

#include "HsVersions.h"

40 41
import GhcPrelude

42
import HsSyn
43
import TyCoRep
44
import TcMType
45
import TcRnMonad
46 47
import TcType
import Type
48
import Coercion
49
import TcEvidence
50
import Name( isSystemName )
51 52 53
import Inst
import TyCon
import TysWiredIn
54
import TysPrim( tYPE )
55
import Var
56
import VarSet
57
import VarEnv
58
import ErrUtils
59
import DynFlags
60
import BasicTypes
61
import Bag
62
import Util
63
import qualified GHC.LanguageExtensions as LangExt
64
import Outputable
65 66

import Control.Monad
67
import Control.Arrow ( second )
68

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

76 77 78 79 80 81 82
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"
83

84
This is used to construct a message of form
85

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

98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the
picture, we have a choice in deciding whether to count the type applications as
proper arguments:

   The function 'f' is applied to one visible type argument
     and two value arguments
   but its type `forall a. a -> a` has only one visible type argument
     and one value argument

Or whether to include the type applications as part of the herald itself:

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

The latter is easier to implement and is arguably easier to understand, so we
choose to implement that option.

115 116
Note [matchExpectedFunTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
117
matchExpectedFunTys checks that a sigma has the form
118 119 120 121 122
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:
123 124
        A lambda expression
        A function definition
125 126
     An operator section

127 128 129 130
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
131
-}
132

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
133
-- Use this one when you have an "expected" type.
134 135
matchExpectedFunTys :: forall a.
                       SDoc   -- See Note [Herald for matchExpectedFunTys]
136
                    -> Arity
137 138 139 140 141
                    -> ExpRhoType  -- deeply skolemised
                    -> ([ExpSigmaType] -> ExpRhoType -> TcM a)
                          -- must fill in these ExpTypes here
                    -> TcM (a, HsWrapper)
-- If    matchExpectedFunTys n ty = (_, wrap)
142
-- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
143 144 145 146 147
--   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
148
  where
149 150 151 152 153
    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
Ben Gamari's avatar
Ben Gamari committed
154
      | Just ty' <- tcView ty = go acc_arg_tys n ty'
155

Simon Peyton Jones's avatar
Simon Peyton Jones committed
156 157
    go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
      = ASSERT( af == VisArg )
158 159 160
        do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
                                      (n-1) res_ty
           ; return ( result
Richard Eisenberg's avatar
Richard Eisenberg committed
161 162 163 164
                    , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) }
      where
        doc = text "When inferring the argument type of a function with type" <+>
              quotes (ppr orig_ty)
165 166

    go acc_arg_tys n ty@(TyVarTy tv)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
167
      | isMetaTyVar tv
168 169 170 171 172 173 174 175 176
      = 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
177
       -- (cf #7869).
178 179 180 181 182 183 184 185 186
       --
       -- 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
187
       -- anyway, because it may be useful. See also #9605.
188 189 190 191
    go acc_arg_tys n ty = addErrCtxtM mk_ctxt $
                          defer acc_arg_tys n (mkCheckExpType ty)

    ------------
192
    defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper)
193
    defer acc_arg_tys n fun_ty
194 195
      = do { more_arg_tys <- replicateM n newInferExpTypeNoInst
           ; res_ty       <- newInferExpTypeInst
196 197 198
           ; 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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
199
           ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
200 201
           ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
                         -- Not a good origin at all :-(
202
           ; return (result, wrap) }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
203

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

216 217
-- Like 'matchExpectedFunTys', but used when you have an "actual" type,
-- for example in function application
218
matchActualFunTys :: SDoc   -- See Note [Herald for matchExpectedFunTys]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
219
                  -> CtOrigin
220
                  -> Maybe (HsExpr GhcRn)   -- the thing with type TcSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
221 222 223
                  -> Arity
                  -> TcSigmaType
                  -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
224
-- If    matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
225
-- then  wrap : ty ~> (t1 -> ... -> tn -> ty_r)
226 227
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
228 229 230

-- | Variant of 'matchActualFunTys' that works when supplied only part
-- (that is, to the right of some arrows) of the full function type
231
matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys]
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
232
                      -> CtOrigin
233
                      -> Maybe (HsExpr GhcRn)  -- the thing with type TcSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
234 235 236 237 238
                      -> Arity
                      -> TcSigmaType
                      -> [TcSigmaType] -- reversed args. See (*) below.
                      -> Arity   -- overall arity of the function, for errs
                      -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
239 240
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
241
  = go arity orig_old_args orig_ty
242 243
-- Does not allocate unnecessary meta variables: if the input already is
-- a function, we just take it apart.  Not only is this efficient,
244
-- it's important for higher rank: the argument might be of form
245
--              (forall a. ty) -> other
246 247 248
-- 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
249 250 251 252 253
-- (*) 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).
254

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
  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
281

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
282
    go n acc_args ty
Ben Gamari's avatar
Ben Gamari committed
283
      | Just ty' <- tcView ty = go n acc_args ty'
284

Simon Peyton Jones's avatar
Simon Peyton Jones committed
285 286
    go n acc_args (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
      = ASSERT( af == VisArg )
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
287
        do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
Richard Eisenberg's avatar
Richard Eisenberg committed
288
           ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
289
                    , arg_ty : tys, ty_r ) }
Richard Eisenberg's avatar
Richard Eisenberg committed
290 291 292
      where
        doc = text "When inferring the argument type of a function with type" <+>
              quotes (ppr orig_ty)
293

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
294
    go n acc_args ty@(TyVarTy tv)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
295
      | isMetaTyVar tv
296
      = do { cts <- readMetaTyVar tv
297
           ; case cts of
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
298
               Indirect ty' -> go n acc_args ty'
299
               Flexi        -> defer n ty }
300 301

       -- In all other cases we bale out into ordinary unification
302
       -- However unlike the meta-tyvar case, we are sure that the
303 304
       -- number of arguments doesn't match arity of the original
       -- type, so we can add a bit more context to the error message
305
       -- (cf #7869).
306 307 308 309 310 311 312 313 314
       --
       -- 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
315
       -- anyway, because it may be useful. See also #9605.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
316
    go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $
317
                       defer n ty
318 319

    ------------
320 321 322
    defer n fun_ty
      = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
           ; res_ty  <- newOpenFlexiTyVarTy
Simon Peyton Jones's avatar
Simon Peyton Jones committed
323
           ; let unif_fun_ty = mkVisFunTys arg_tys res_ty
324
           ; co <- unifyType mb_thing fun_ty unif_fun_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
325
           ; return (mkWpCastN co, arg_tys, res_ty) }
326 327

    ------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
328 329
    mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
    mk_ctxt arg_tys res_ty env
Simon Peyton Jones's avatar
Simon Peyton Jones committed
330
      = do { let ty = mkVisFunTys arg_tys res_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
331 332 333 334 335
           ; (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
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
           ; 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]
354

355
----------------------
356
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
357
-- Special case for lists
358
matchExpectedListTy exp_ty
batterseapower's avatar
batterseapower committed
359 360
 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
      ; return (co, elt_ty) }
361

362
---------------------
dreixel's avatar
dreixel committed
363
matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
364
                      -> TcRhoType            -- orig_ty
365
                      -> TcM (TcCoercionN,    -- T k1 k2 k3 a b c ~N orig_ty
dreixel's avatar
dreixel committed
366
                              [TcSigmaType])  -- Element types, k1 k2 k3 a b c
367

368 369 370
-- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
371
-- Postcondition: (T k1 k2 k3 a b c) is well-kinded
372 373

matchExpectedTyConApp tc orig_ty
374
  = ASSERT(tc /= funTyCon) go orig_ty
375
  where
376
    go ty
Ben Gamari's avatar
Ben Gamari committed
377
       | Just ty' <- tcView ty
378 379
       = go ty'

380
    go ty@(TyConApp tycon args)
381
       | tc == tycon  -- Common case
382
       = return (mkTcNomReflCo ty, args)
383 384

    go (TyVarTy tv)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
385
       | isMetaTyVar tv
386 387 388
       = do { cts <- readMetaTyVar tv
            ; case cts of
                Indirect ty -> go ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
389
                Flexi       -> defer }
390

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
391
    go _ = defer
392 393 394 395 396 397

    -- 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)
398
    -- where data T a = MkT a
Gabor Greif's avatar
Gabor Greif committed
399
    -- Then we don't want to instantiate T's data constructors with
400 401
    --    (a::*) ~ Maybe
    -- because that'll make types that are utterly ill-kinded.
402
    -- This happened in #7368
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
403
    defer
404
      = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc)
Richard Eisenberg's avatar
Richard Eisenberg committed
405
           ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
406 407
           ; let args = mkTyVarTys arg_tvs
                 tc_template = mkTyConApp tc args
408
           ; co <- unifyType Nothing tc_template orig_ty
409
           ; return (co, args) }
410

411 412
----------------------
matchExpectedAppTy :: TcRhoType                         -- orig_ty
413
                   -> TcM (TcCoercion,                   -- m a ~N orig_ty
414 415 416
                           (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
417

418 419
matchExpectedAppTy orig_ty
  = go orig_ty
420
  where
421
    go ty
Ben Gamari's avatar
Ben Gamari committed
422
      | Just ty' <- tcView ty = go ty'
423

424
      | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
425
      = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
426

427
    go (TyVarTy tv)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
428
      | isMetaTyVar tv
429 430 431
      = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty -> go ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
432
               Flexi       -> defer }
Ian Lynagh's avatar
Ian Lynagh committed
433

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

436
    -- Defer splitting by generating an equality constraint
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
437 438 439
    defer
      = do { ty1 <- newFlexiTyVarTy kind1
           ; ty2 <- newFlexiTyVarTy kind2
440
           ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
441
           ; return (co, (ty1, ty2)) }
442

443
    orig_kind = tcTypeKind orig_ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
444
    kind1 = mkVisFunTy liftedTypeKind orig_kind
445 446
    kind2 = liftedTypeKind    -- m :: * -> k
                              -- arg type :: *
447

Austin Seipp's avatar
Austin Seipp committed
448 449 450
{-
************************************************************************
*                                                                      *
Ian Lynagh's avatar
Ian Lynagh committed
451
                Subsumption checking
Austin Seipp's avatar
Austin Seipp committed
452 453
*                                                                      *
************************************************************************
454

455 456 457 458
Note [Subsumption checking: tcSubType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All the tcSubType calls have the form
                tcSubType actual_ty expected_ty
459
which checks
Ian Lynagh's avatar
Ian Lynagh committed
460
                actual_ty <= expected_ty
461

462
That is, that a value of type actual_ty is acceptable in
463 464 465
a place expecting a value of type expected_ty.  I.e. that

    actual ty   is more polymorphic than   expected_ty
466

Ian Lynagh's avatar
Ian Lynagh committed
467 468
It returns a coercion function
        co_fn :: actual_ty ~ expected_ty
469
which takes an HsExpr of type actual_ty into one of type
470 471
expected_ty.

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
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.

487 488 489 490
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
491
more predictable type inference.
492 493 494 495 496 497 498

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
499
That is why tc_sub_type starts with a call to tcSkolemise (which does the
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515
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
516
tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of
517 518 519
HsWrapper.

Another powerful reason for doing this co/contra stuff is visible
520
in #9569, involving instantiation of constraint variables,
521 522 523 524 525 526 527 528 529 530 531 532 533
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
534
-}
535

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
536 537 538

-- | Call this variant when you are in a higher-rank situation and
-- you know the right-hand type is deeply skolemised.
539 540
tcSubTypeHR :: CtOrigin               -- ^ of the actual type
            -> Maybe (HsExpr GhcRn)   -- ^ If present, it has type ty_actual
541
            -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
542 543
tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt

544 545 546 547 548 549 550
------------------------
tcSubTypeET :: CtOrigin -> UserTypeCtxt
            -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-- If wrap = tc_sub_type_et t1 t2
--    => wrap :: t1 ~> t2
tcSubTypeET orig ctxt (Check ty_actual) ty_expected
  = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected
551
  where
552 553
    eq_orig = TypeEqOrigin { uo_actual   = ty_expected
                           , uo_expected = ty_actual
554 555
                           , uo_thing    = Nothing
                           , uo_visible  = True }
556

557 558
tcSubTypeET _ _ (Infer inf_res) ty_expected
  = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected )
559 560
      -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never
      -- has the ir_inst field set.  Reason: in patterns (which is what
Sasa Bogicevic's avatar
Sasa Bogicevic committed
561
      -- tcSubTypeET is used for) do not aggressively instantiate
562 563 564 565
    do { co <- fill_infer_result ty_expected inf_res
               -- Since ir_inst is false, we can skip fillInferResult
               -- and go straight to fill_infer_result

566 567 568
       ; return (mkWpCastN (mkTcSymCo co)) }

------------------------
569 570 571
tcSubTypeO :: CtOrigin      -- ^ of the actual type
           -> UserTypeCtxt  -- ^ of the expected type
           -> TcSigmaType
572
           -> ExpRhoType
573
           -> TcM HsWrapper
574
tcSubTypeO orig ctxt ty_actual ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
575 576 577 578 579
  = addSubTypeCtxt ty_actual ty_expected $
    do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig
                                       , pprUserTypeCtxt ctxt
                                       , ppr ty_actual
                                       , ppr ty_expected ])
580
       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
581

582
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
583
addSubTypeCtxt ty_actual ty_expected thing_inside
584 585 586
 | 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
587 588 589 590 591
 | otherwise
 = addErrCtxtM mk_msg thing_inside
  where
    mk_msg tidy_env
      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
592 593 594 595 596 597 598
                   -- 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
599
           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
600
           ; let msg = vcat [ hang (text "When checking that:")
601
                                 4 (ppr ty_actual)
602
                            , nest 2 (hang (text "is more polymorphic than:")
603 604 605 606 607 608 609
                                         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

610 611 612
tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- Checks that actual <= expected
-- Returns HsWrapper :: actual ~ expected
613 614
tcSubType_NC ctxt ty_actual ty_expected
  = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
615
       ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected }
616
  where
617 618
    origin = TypeEqOrigin { uo_actual   = ty_actual
                          , uo_expected = ty_expected
619 620
                          , uo_thing    = Nothing
                          , uo_visible  = True }
621

622 623 624 625 626 627
tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised (hence "DS")
tcSubTypeDS orig ctxt ty_actual ty_expected
  = addSubTypeCtxt ty_actual ty_expected $
    do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
628
       ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected }
629

630
tcSubTypeDS_NC_O :: CtOrigin   -- origin used for instantiation only
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
631
                 -> UserTypeCtxt
632
                 -> Maybe (HsExpr GhcRn)
633
                 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
634 635
-- Just like tcSubType, but with the additional precondition that
-- ty_expected is deeply skolemised
636 637
tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected
  = case ty_expected of
638
      Infer inf_res -> fillInferResult inst_orig ty_actual inf_res
639 640 641
      Check ty      -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty
         where
           eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty
642 643
                                  , uo_thing  = ppr <$> m_thing
                                  , uo_visible = True }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
644

645
---------------
646 647 648
tc_sub_tc_type :: CtOrigin   -- used when calling uType
               -> CtOrigin   -- used when instantiating
               -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
649 650
-- If wrap = tc_sub_type t1 t2
--    => wrap :: t1 ~> t2
651
tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
652 653
  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
  , not (possibly_poly ty_actual)
654 655 656 657
  = do { traceTc "tc_sub_tc_type (drop to equality)" $
         vcat [ text "ty_actual   =" <+> ppr ty_actual
              , text "ty_expected =" <+> ppr ty_expected ]
       ; mkWpCastN <$>
658
         uType TypeLevel eq_orig ty_actual ty_expected }
659 660 661 662 663 664 665

  | otherwise   -- This is the general case
  = do { traceTc "tc_sub_tc_type (general case)" $
         vcat [ text "ty_actual   =" <+> ppr ty_actual
              , text "ty_expected =" <+> ppr ty_expected ]
       ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $
                                                   \ _ sk_rho ->
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
666 667
                                  tc_sub_type_ds eq_orig inst_orig ctxt
                                                 ty_actual sk_rho
668
       ; return (sk_wrap <.> inner_wrap) }
669
  where
670
    possibly_poly ty
671
      | isForAllTy ty                        = True
672
      | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
673 674 675 676
      | otherwise                            = False
      -- NB *not* tcSplitFunTy, because here we want
      -- to decompose type-class arguments too

677 678 679 680 681 682 683 684
    definitely_poly ty
      | (tvs, theta, tau) <- tcSplitSigmaTy ty
      , (tv:_) <- tvs
      , null theta
      , isInsolubleOccursCheck NomEq tv tau
      = True
      | otherwise
      = False
685 686 687 688 689 690 691 692 693 694 695

{- Note [Don't skolemise unnecessarily]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are trying to solve
    (Char->Char) <= (forall a. a->a)
We could skolemise the 'forall a', and then complain
that (Char ~ a) is insoluble; but that's a pretty obscure
error.  It's better to say that
    (Char->Char) ~ (forall a. a->a)
fails.

696 697 698 699 700
So roughly:
 * if the ty_expected has an outermost forall
      (i.e. skolemisation is the next thing we'd do)
 * and the ty_actual has no top-level polymorphism (but looking deeply)
then we can revert to simple equality.  But we need to be careful.
Gabor Greif's avatar
Gabor Greif committed
701
These examples are all fine:
702 703 704 705 706 707 708 709 710 711 712 713 714 715 716

 * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
      Polymorphism is buried in ty_actual

 * (Char->Char) <= (forall a. Char -> Char)
      ty_expected isn't really polymorphic

 * (Char->Char) <= (forall a. (a~Char) => a -> a)
      ty_expected isn't really polymorphic

 * (Char->Char) <= (forall a. F [a] Char -> Char)
                   where type instance F [x] t = t
     ty_expected isn't really polymorphic

If we prematurely go to equality we'll reject a program we should
717
accept (e.g. #13752).  So the test (which is only to improve
Gabor Greif's avatar
Gabor Greif committed
718
error message) is very conservative:
719 720
 * ty_actual is /definitely/ monomorphic
 * ty_expected is /definitely/ polymorphic
721
-}
722 723

---------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
724 725 726
tc_sub_type_ds :: CtOrigin    -- used when calling uType
               -> CtOrigin    -- used when instantiating
               -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper
727 728 729 730
-- If wrap = tc_sub_type_ds t1 t2
--    => wrap :: t1 ~> t2
-- Here is where the work actually happens!
-- Precondition: ty_expected is deeply skolemised
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
731
tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
732 733 734 735
  = do { traceTc "tc_sub_type_ds" $
         vcat [ text "ty_actual   =" <+> ppr ty_actual
              , text "ty_expected =" <+> ppr ty_expected ]
       ; go ty_actual ty_expected }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
736
  where
Ben Gamari's avatar
Ben Gamari committed
737 738
    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
739 740 741 742 743 744 745 746

    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
747
               Unfilled _   -> unify }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
748

749 750 751 752
    -- 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
Sasa Bogicevic's avatar
Sasa Bogicevic committed
753
    -- simply do not have decent story for impredicative types), but it
754
    -- caused #12616 because (also bizarrely) 'deriving' code had
755
    -- -XImpredicativeTypes on.  I deleted the entire case.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
756

Simon Peyton Jones's avatar
Simon Peyton Jones committed
757 758
    go (FunTy { ft_af = VisArg, ft_arg = act_arg, ft_res = act_res })
       (FunTy { ft_af = VisArg, ft_arg = exp_arg, ft_res = exp_res })
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
759
      = -- See Note [Co/contra-variance of subsumption checking]
760 761 762
        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt       act_res exp_res
           ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg
                         -- GenSigCtxt: See Note [Setting the argument context]
Richard Eisenberg's avatar
Richard Eisenberg committed
763
           ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
764 765
               -- arg_wrap :: exp_arg ~> act_arg
               -- res_wrap :: act-res ~> exp_res
Richard Eisenberg's avatar
Richard Eisenberg committed
766
      where
767
        given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
Richard Eisenberg's avatar
Richard Eisenberg committed
768 769
        doc = text "When checking that" <+> quotes (ppr ty_actual) <+>
              text "is more polymorphic than" <+> quotes (ppr ty_expected)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
770 771 772 773 774

    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
775 776
           ; body_wrap <- tc_sub_type_ds
                            (eq_orig { uo_actual = in_rho
777
                                     , uo_expected = ty_expected })
778
                            inst_orig ctxt in_rho ty_e
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
779 780 781
           ; return (body_wrap <.> in_wrap) }

      | otherwise   -- Revert to unification
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
782 783 784
      = 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.
785 786 787 788
         -- 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
789 790 791

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
792
                           -- If we haven't recurred through an arrow, then
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
793 794 795 796 797
                           -- 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
798
                                TypeEqOrigin { uo_actual   = orig_ty_actual }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
799 800
                                  |  orig_ty_actual `tcEqType` ty_actual
                                  ,  not (isIdHsWrapper wrap)
801
                                  -> eq_orig { uo_actual = rho_a }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
802 803
                                _ -> eq_orig

804
                        ; cow <- uType TypeLevel eq_orig' rho_a ty_expected
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
805 806
                        ; return (mkWpCastN cow <.> wrap) }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
807 808

     -- use versions without synonyms expanded
809
    unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected
810

811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837
{- Note [Settting the argument context]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider we are doing the ambiguity check for the (bogus)
  f :: (forall a b. C b => a -> a) -> Int

We'll call
   tcSubType ((forall a b. C b => a->a) -> Int )
             ((forall a b. C b => a->a) -> Int )

with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
on the argument type of the (->) -- and at that point we want to switch
to a UserTypeCtxt of GenSigCtxt.  Why?

* Error messages.  If we stick with FunSigCtxt we get errors like
     * Could not deduce: C b
       from the context: C b0
        bound by the type signature for:
            f :: forall a b. C b => a->a
  But of course f does not have that type signature!
  Example tests: T10508, T7220a, Simple14

* Implications. We may decide to build an implication for the whole
  ambiguity check, but we don't need one for each level within it,
  and TcUnify.alwaysBuildImplication checks the UserTypeCtxt.
  See Note [When to build an implication]
-}

838
-----------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
839 840
-- needs both un-type-checked (for origins) and type-checked (for wrapping)
-- expressions
841 842
tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
             -> TcM (HsExpr GhcTcId)
843
tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
844 845 846

-- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
-- convenient.
847
tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
848
               -> TcM (HsExpr GhcTcId)
849
tcWrapResultO orig rn_expr expr actual_ty res_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
850 851 852
  = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                      , text "Expected:" <+> ppr res_ty ])
       ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt
853
                                 (Just rn_expr) actual_ty res_ty
854
       ; return (mkHsWrap cow expr) }
855

856 857 858 859 860 861 862

{- **********************************************************************
%*                                                                      *
            ExpType functions: tcInfer, fillInferResult
%*                                                                      *
%********************************************************************* -}

863 864
-- | Infer a type using a fresh ExpType
-- See also Note [ExpType] in TcMType
865 866 867 868 869 870 871 872 873 874
-- Does not attempt to instantiate the inferred type
tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
tcInferNoInst = tcInfer False

tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType)
tcInferInst = tcInfer True

tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
tcInfer instantiate tc_check
  = do { res_ty <- newInferExpType instantiate
875 876 877
       ; result <- tc_check res_ty
       ; res_ty <- readExpType res_ty
       ; return (result, res_ty) }
878

879 880
fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
-- If wrap = fillInferResult t1 t2
881 882
--    => wrap :: t1 ~> t2
-- See Note [Deep instantiation of InferResult]
883
fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me })
884 885
  | instantiate_me
  = do { (wrap, rho) <- deeplyInstantiate orig ty
886
       ; co <- fill_infer_result rho inf_res
887 888 889
       ; return (mkWpCastN co <.> wrap) }

  | otherwise
890
  = do { co <- fill_infer_result ty inf_res
891 892
       ; return (mkWpCastN co) }

893 894
fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN
-- If wrap = fill_infer_result t1 t2
895
--    => wrap :: t1 ~> t2
896
fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
897 898
                            , ir_ref = ref })
  = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
899 900 901 902

       ; traceTc "Filling ExpType" $
         ppr u <+> text ":=" <+> ppr ty_to_fill_with

903 904 905
       ; when debugIsOn (check_hole ty_to_fill_with)

       ; writeTcRef ref (Just ty_to_fill_with)
906

907
       ; return ty_co }
908 909
  where
    check_hole ty   -- Debug check only
910
      = do { let ty_lvl = tcTypeLevel ty
911
           ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
912
                       ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
913
                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
914 915 916 917 918 919 920 921 922 923 924 925 926 927
           ; cts <- readTcRef ref
           ; case cts of
               Just already_there -> pprPanic "writeExpType"
                                       (vcat [ ppr u
                                             , ppr ty
                                             , ppr already_there ])
               Nothing -> return () }

{- Note [Deep instantiation of InferResult]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In some cases we want to deeply instantiate before filling in
an InferResult, and in some cases not.  That's why InferReult
has the ir_inst flag.

928
* ir_inst = True: deeply instantiate
929 930 931 932 933 934 935 936

  Consider
    f x = (*)
  We want to instantiate the type of (*) before returning, else we
  will infer the type
    f :: forall {a}. a -> forall b. Num b => b -> b -> b
  This is surely confusing for users.

Sasa Bogicevic's avatar
Sasa Bogicevic committed
937
  And worse, the monomorphism restriction won't work properly. The MR is
938 939 940