ghc/compiler/typecheck/TcUnify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Type subsumption and unification}
   5
   6 \begin{code}
   7 module TcUnify (
   8         -- Full-blown subsumption
   9   tcSubPat, tcSubExp, tcSub, tcGen,
  10   checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
  11
  12         -- Various unifications
  13   unifyTauTy, unifyTauTyList, unifyTheta,
  14   unifyKind, unifyKinds, unifyFunKind,
  15   checkExpectedKind,
  16
  17   --------------------------------
  18   -- Holes
  19   Expected(..), tcInfer, readExpectedType,
  20   zapExpectedType, zapExpectedTo, zapExpectedBranches,
  21   subFunTys,     unifyFunTys,
  22   zapToListTy,   unifyListTy,
  23   zapToTyConApp, unifyTyConApp,
  24   unifyAppTy
  25   ) where
  26
  27 #include "HsVersions.h"
  28
  29 -- gaw 2004
  30 import HsSyn            ( HsExpr(..) , MatchGroup(..), hsLMatchPats )
  31 import TcHsSyn          ( mkHsLet, mkHsDictLam,
  32                           ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
  33 import TypeRep          ( Type(..), PredType(..), TyNote(..) )
  34
  35 import TcRnMonad         -- TcType, amongst others
  36 import TcType           ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
  37                           TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
  38                           SkolemInfo( GenSkol ), MetaDetails(..),
  39                           pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
  40                           tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
  41                           tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
  42                           typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
  43                           tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
  44                           pprType, tidySkolemTyVar, isSkolemTyVar )
  45 import Kind             ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
  46                           openTypeKind, liftedTypeKind, mkArrowKind,
  47                           isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
  48                           isSubKind, pprKind, splitKindFunTys )
  49 import Inst             ( newDicts, instToId, tcInstCall )
  50 import TcMType          ( condLookupTcTyVar, LookupTyVarResult(..),
  51                           tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
  52                           newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV,
  53                           readKindVar, writeKindVar )
  54 import TcSimplify       ( tcSimplifyCheck )
  55 import TcEnv            ( tcGetGlobalTyVars, findGlobals )
  56 import TyCon            ( TyCon, tyConArity, tyConTyVars )
  57 import TysWiredIn       ( listTyCon )
  58 import Id               ( Id, mkSysLocal )
  59 import Var              ( Var, varName, tyVarKind )
  60 import VarSet           ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
  61 import VarEnv
  62 import Name             ( isSystemName, mkSysTvName )
  63 import ErrUtils         ( Message )
  64 import SrcLoc           ( noLoc )
  65 import BasicTypes       ( Arity )
  66 import Util             ( notNull, equalLength )
  67 import Outputable
  68 \end{code}
  69
  70 Notes on holes
  71 ~~~~~~~~~~~~~~
  72 * A hole is always filled in with an ordinary type, not another hole.
  73
  74 %************************************************************************
  75 %*                                                                      *
  76 \subsection{'hole' type variables}
  77 %*                                                                      *
  78 %************************************************************************
  79
  80 \begin{code}
  81 newHole = newMutVar (error "Empty hole in typechecker")
  82
  83 tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
  84 tcInfer tc_infer
  85   = do  { hole <- newHole
  86         ; res <- tc_infer (Infer hole)
  87         ; res_ty <- readMutVar hole
  88         ; return (res, res_ty) }
  89
  90 readExpectedType :: Expected ty -> TcM ty
  91 readExpectedType (Infer hole) = readMutVar hole
  92 readExpectedType (Check ty)   = returnM ty
  93
  94 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
  95 -- In the inference case, ensure we have a monotype
  96 -- (including an unboxed tuple)
  97 zapExpectedType (Infer hole) kind
  98   = do { ty <- newTyFlexiVarTy kind ;
  99          writeMutVar hole ty ;
 100          return ty }
 101
 102 zapExpectedType (Check ty) kind
 103   | typeKind ty `isSubKind` kind = return ty
 104   | otherwise                    = do { ty1 <- newTyFlexiVarTy kind
 105                                       ; unifyTauTy ty1 ty
 106                                       ; return ty }
 107         -- The unify is to ensure that 'ty' has the desired kind
 108         -- For example, in (case e of r -> b) we push an OpenTypeKind
 109         -- type variable
 110
 111 zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
 112 -- If there is more than one branch in a case expression,
 113 -- and exp_ty is a 'hole', all branches must be types, not type schemes,
 114 -- otherwise the order in which we check them would affect the result.
 115 zapExpectedBranches (MatchGroup [match] _) exp_ty
 116    = return exp_ty      -- One branch
 117 zapExpectedBranches matches (Check ty)
 118   = return (Check ty)
 119 zapExpectedBranches matches (Infer hole)
 120   = do  {       -- Many branches, and inference mode,
 121                 -- so switch to checking mode with a monotype
 122           ty <- newTyFlexiVarTy openTypeKind
 123         ; writeMutVar hole ty
 124         ; return (Check ty) }
 125
 126 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
 127 zapExpectedTo (Check ty1)  ty2 = unifyTauTy ty1 ty2
 128 zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
 129         -- See Note [Zonk return type]
 130
 131 instance Outputable ty => Outputable (Expected ty) where
 132   ppr (Check ty)   = ptext SLIT("Expected type") <+> ppr ty
 133   ppr (Infer hole) = ptext SLIT("Inferring type")
 134 \end{code}
 135
 136
 137 %************************************************************************
 138 %*                                                                      *
 139 \subsection[Unify-fun]{@unifyFunTy@}
 140 %*                                                                      *
 141 %************************************************************************
 142
 143 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
 144 creation of type variables.
 145
 146 * subFunTy is used when we might be faced with a "hole" type variable,
 147   in which case we should create two new holes.
 148
 149 * unifyFunTy is used when we expect to encounter only "ordinary"
 150   type variables, so we should create new ordinary type variables
 151
 152 \begin{code}
 153 subFunTys :: MatchGroup name
 154           -> Expected TcRhoType         -- Fail if ty isn't a function type
 155           -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
 156           -> TcM a
 157
 158 subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
 159   =     -- This is the interesting case
 160     ASSERT( null null_matches )
 161     do  { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
 162         ; res_hole  <- newHole
 163
 164                 -- Do the business
 165         ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
 166
 167                 -- Extract the answers
 168         ; arg_tys <- mapM readMutVar pat_holes
 169         ; res_ty  <- readMutVar res_hole
 170
 171                 -- Write the answer into the incoming hole
 172         ; writeMutVar hole (mkFunTys arg_tys res_ty)
 173
 174                 -- And return the answer
 175         ; return res }
 176
 177 subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside
 178   = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches )
 179         -- Assertion just checks that all the matches have the same number of pats
 180     do  { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty
 181         ; thing_inside (map Check pat_tys) (Check res_ty) }
 182
 183 unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
 184 -- Fail if ty isn't a function type, otherwise return arg and result types
 185 -- The result types are guaranteed wobbly if the argument is wobbly
 186 --
 187 -- Does not allocate unnecessary meta variables: if the input already is
 188 -- a function, we just take it apart.  Not only is this efficient, it's important
 189 -- for  (a) higher rank: the argument might be of form
 190 --              (forall a. ty) -> other
 191 --          If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
 192 --          blow up with the meta var meets the forall
 193 --
 194 --      (b) GADTs: if the argument is not wobbly we do not want the result to be
 195
 196 unifyFunTys arity ty = unify_fun_ty True arity ty
 197
 198 unify_fun_ty use_refinement arity ty
 199   | arity == 0
 200   = do  { res_ty <- wobblify use_refinement ty
 201         ; return ([], ty) }
 202
 203 unify_fun_ty use_refinement arity (NoteTy _ ty)
 204   = unify_fun_ty use_refinement arity ty
 205
 206 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
 207   = do  { details <- condLookupTcTyVar use_refinement tv
 208         ; case details of
 209             IndirectTv use' ty' -> unify_fun_ty use' arity ty'
 210             other               -> unify_fun_help arity ty
 211         }
 212
 213 unify_fun_ty use_refinement arity ty
 214   = case tcSplitFunTy_maybe ty of
 215         Just (arg,res) -> do { arg'          <- wobblify use_refinement arg
 216                              ; (args', res') <- unify_fun_ty use_refinement (arity-1) res
 217                              ; return (arg':args', res') }
 218
 219         Nothing -> unify_fun_help arity ty
 220         -- Usually an error, but ty could be (a Int Bool), which can match
 221
 222 unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
 223 unify_fun_help arity ty
 224   = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
 225        ; res <- newTyFlexiVarTy openTypeKind
 226        ; unifyTauTy ty (mkFunTys args res)
 227        ; return (args, res) }
 228 \end{code}
 229
 230 \begin{code}
 231 ----------------------
 232 zapToTyConApp :: TyCon                  -- T :: k1 -> ... -> kn -> *
 233               -> Expected TcSigmaType   -- Expected type (T a b c)
 234               -> TcM [TcType]           -- Element types, a b c
 235   -- Insists that the Expected type is not a forall-type
 236
 237 zapToTyConApp tc (Check ty)
 238    = unifyTyConApp tc ty         -- NB: fails for a forall-type
 239 zapToTyConApp tc (Infer hole)
 240   = do  { (tc_app, elt_tys) <- newTyConApp tc
 241         ; writeMutVar hole tc_app
 242         ; return elt_tys }
 243
 244 zapToListTy :: Expected TcType -> TcM TcType    -- Special case for lists
 245 zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
 246                         ; return elt_ty }
 247
 248 ----------------------
 249 unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
 250 unifyTyConApp tc ty = unify_tc_app True tc ty
 251         -- Add a boolean flag to remember whether to use
 252         -- the type refinement or not
 253
 254 unifyListTy :: TcType -> TcM TcType     -- Special case for lists
 255 unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
 256                         ; return elt_ty }
 257
 258 ----------
 259 unify_tc_app use_refinement tc (NoteTy _ ty)
 260   = unify_tc_app use_refinement tc ty
 261
 262 unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
 263   = do  { details <- condLookupTcTyVar use_refinement tyvar
 264         ; case details of
 265             IndirectTv use' ty' -> unify_tc_app use' tc ty'
 266             other               -> unify_tc_app_help tc ty
 267         }
 268
 269 unify_tc_app use_refinement tc ty
 270   | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
 271     tycon == tc
 272   = ASSERT( tyConArity tycon == length arg_tys )        -- ty::*
 273     mapM (wobblify use_refinement) arg_tys
 274
 275 unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
 276
 277 unify_tc_app_help tc ty         -- Revert to ordinary unification
 278   = do  { (tc_app, arg_tys) <- newTyConApp tc
 279         ; if not (isTauTy ty) then      -- Can happen if we call zapToTyConApp tc (forall a. ty)
 280              unifyMisMatch ty tc_app
 281           else do
 282         { unifyTauTy ty tc_app
 283         ; returnM arg_tys } }
 284
 285
 286 ----------------------
 287 unifyAppTy :: TcType                    -- Type to split: m a
 288            -> TcM (TcType, TcType)      -- (m,a)
 289 -- Assumes (m:*->*)
 290
 291 unifyAppTy ty = unify_app_ty True ty
 292
 293 unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty
 294
 295 unify_app_ty use ty@(TyVarTy tyvar)
 296   = do  { details <- condLookupTcTyVar use tyvar
 297         ; case details of
 298             IndirectTv use' ty' -> unify_app_ty use' ty'
 299             other               -> unify_app_ty_help ty
 300         }
 301
 302 unify_app_ty use ty
 303   | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
 304   = do  { fun' <- wobblify use fun_ty
 305         ; arg' <- wobblify use arg_ty
 306         ; return (fun', arg') }
 307
 308   | otherwise = unify_app_ty_help ty
 309
 310 unify_app_ty_help ty            -- Revert to ordinary unification
 311   = do  { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind)
 312         ; arg_ty <- newTyFlexiVarTy liftedTypeKind
 313         ; unifyTauTy (mkAppTy fun_ty arg_ty) ty
 314         ; return (fun_ty, arg_ty) }
 315
 316
 317 ----------------------
 318 wobblify :: Bool        -- True <=> don't wobblify
 319          -> TcTauType
 320          -> TcM TcTauType
 321 -- Return a wobbly type.  At the moment we do that by
 322 -- allocating a fresh meta type variable.
 323 wobblify True  ty = return ty
 324 wobblify False ty = do  { uniq <- newUnique
 325                         ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
 326                                              (typeKind ty)
 327                                              (Indirect ty)
 328                         ; return (mkTyVarTy tv) }
 329
 330 ----------------------
 331 newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
 332 newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
 333                     ; return (mkTyConApp tc args, args) }
 334 \end{code}
 335
 336
 337 %************************************************************************
 338 %*                                                                      *
 339 \subsection{Subsumption}
 340 %*                                                                      *
 341 %************************************************************************
 342
 343 All the tcSub calls have the form
 344
 345                 tcSub expected_ty offered_ty
 346 which checks
 347                 offered_ty <= expected_ty
 348
 349 That is, that a value of type offered_ty is acceptable in
 350 a place expecting a value of type expected_ty.
 351
 352 It returns a coercion function
 353         co_fn :: offered_ty -> expected_ty
 354 which takes an HsExpr of type offered_ty into one of type
 355 expected_ty.
 356
 357 \begin{code}
 358 -----------------------
 359 -- tcSubExp is used for expressions
 360 tcSubExp :: Expected TcRhoType -> TcRhoType  -> TcM ExprCoFn
 361
 362 tcSubExp (Infer hole) offered_ty
 363   = do { offered' <- zonkTcType offered_ty
 364         -- Note [Zonk return type]
 365         -- zonk to take advantage of the current GADT type refinement.
 366         -- If we don't we get spurious "existential type variable escapes":
 367         --      case (x::Maybe a) of
 368         --        Just b (y::b) -> y
 369         -- We need the refinement [b->a] to be applied to the result type
 370         ; writeMutVar hole offered'
 371         ; return idCoercion }
 372
 373 tcSubExp (Check expected_ty) offered_ty
 374   = tcSub expected_ty offered_ty
 375
 376 -----------------------
 377 -- tcSubPat is used for patterns
 378 tcSubPat :: TcSigmaType                 -- Pattern type signature
 379          -> Expected TcSigmaType        -- Type from context
 380          -> TcM ()
 381 -- In patterns we insist on an exact match; hence no CoFn returned
 382 --      See Note [Pattern coercions] in TcPat
 383 -- However, we can't call unify directly, because both types might be
 384 -- polymorphic; hence the call to tcSub, followed by a check for
 385 -- the identity coercion
 386
 387 tcSubPat sig_ty (Infer hole)
 388   = do { sig_ty' <- zonkTcType sig_ty
 389         ; writeMutVar hole sig_ty'      -- See notes with tcSubExp above
 390         ; return () }
 391
 392 tcSubPat sig_ty (Check exp_ty)
 393   = do  { co_fn <- tcSub sig_ty exp_ty
 394
 395         ; if isIdCoercion co_fn then
 396                 return ()
 397           else
 398                 unifyMisMatch sig_ty exp_ty }
 399 \end{code}
 400
 401
 402
 403 %************************************************************************
 404 %*                                                                      *
 405         tcSub: main subsumption-check code
 406 %*                                                                      *
 407 %************************************************************************
 408
 409 No holes expected now.  Add some error-check context info.
 410
 411 \begin{code}
 412 -----------------
 413 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn     -- Locally used only
 414         -- tcSub exp act checks that
 415         --      act <= exp
 416 tcSub expected_ty actual_ty
 417   = traceTc (text "tcSub" <+> details)          `thenM_`
 418     addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
 419                 (tc_sub expected_ty expected_ty actual_ty actual_ty)
 420   where
 421     details = vcat [text "Expected:" <+> ppr expected_ty,
 422                     text "Actual:  " <+> ppr actual_ty]
 423
 424 -----------------
 425 tc_sub :: TcSigmaType           -- expected_ty, before expanding synonyms
 426        -> TcSigmaType           --              ..and after
 427        -> TcSigmaType           -- actual_ty, before
 428        -> TcSigmaType           --              ..and after
 429        -> TcM ExprCoFn
 430
 431 -----------------------------------
 432 -- Expand synonyms
 433 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
 434 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
 435
 436 -----------------------------------
 437 -- Generalisation case
 438 --      actual_ty:   d:Eq b => b->b
 439 --      expected_ty: forall a. Ord a => a->a
 440 --      co_fn e      /\a. \d2:Ord a. let d = eqFromOrd d2 in e
 441
 442 -- It is essential to do this *before* the specialisation case
 443 -- Example:  f :: (Eq a => a->a) -> ...
 444 --           g :: Ord b => b->b
 445 -- Consider  f g !
 446
 447 tc_sub exp_sty expected_ty act_sty actual_ty
 448   | isSigmaTy expected_ty
 449   = tcGen expected_ty (tyVarsOfType actual_ty) (
 450         -- It's really important to check for escape wrt the free vars of
 451         -- both expected_ty *and* actual_ty
 452         \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
 453     )                           `thenM` \ (gen_fn, co_fn) ->
 454     returnM (gen_fn <.> co_fn)
 455
 456 -----------------------------------
 457 -- Specialisation case:
 458 --      actual_ty:   forall a. Ord a => a->a
 459 --      expected_ty: Int -> Int
 460 --      co_fn e =    e Int dOrdInt
 461
 462 tc_sub exp_sty expected_ty act_sty actual_ty
 463   | isSigmaTy actual_ty
 464   = tcInstCall InstSigOrigin actual_ty          `thenM` \ (inst_fn, _, body_ty) ->
 465     tc_sub exp_sty expected_ty body_ty body_ty  `thenM` \ co_fn ->
 466     returnM (co_fn <.> inst_fn)
 467
 468 -----------------------------------
 469 -- Function case
 470
 471 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
 472   = tcSub_fun exp_arg exp_res act_arg act_res
 473
 474 -----------------------------------
 475 -- Type variable meets function: imitate
 476 --
 477 -- NB 1: we can't just unify the type variable with the type
 478 --       because the type might not be a tau-type, and we aren't
 479 --       allowed to instantiate an ordinary type variable with
 480 --       a sigma-type
 481 --
 482 -- NB 2: can we short-cut to an error case?
 483 --       when the arg/res is not a tau-type?
 484 -- NO!  e.g.   f :: ((forall a. a->a) -> Int) -> Int
 485 --      then   x = (f,f)
 486 --      is perfectly fine, because we can instantiate f's type to a monotype
 487 --
 488 -- However, we get can get jolly unhelpful error messages.
 489 --      e.g.    foo = id runST
 490 --
 491 --    Inferred type is less polymorphic than expected
 492 --      Quantified type variable `s' escapes
 493 --      Expected type: ST s a -> t
 494 --      Inferred type: (forall s1. ST s1 a) -> a
 495 --    In the first argument of `id', namely `runST'
 496 --    In a right-hand side of function `foo': id runST
 497 --
 498 -- I'm not quite sure what to do about this!
 499
 500 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
 501   = do  { ([act_arg], act_res) <- unifyFunTys 1 act_ty
 502         ; tcSub_fun exp_arg exp_res act_arg act_res }
 503
 504 tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
 505   = do  { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
 506         ; tcSub_fun exp_arg exp_res act_arg act_res }
 507
 508 -----------------------------------
 509 -- Unification case
 510 -- If none of the above match, we revert to the plain unifier
 511 tc_sub exp_sty expected_ty act_sty actual_ty
 512   = uTys True exp_sty expected_ty True act_sty actual_ty        `thenM_`
 513     returnM idCoercion
 514 \end{code}
 515
 516 \begin{code}
 517 tcSub_fun exp_arg exp_res act_arg act_res
 518   = tc_sub act_arg act_arg exp_arg exp_arg      `thenM` \ co_fn_arg ->
 519     tc_sub exp_res exp_res act_res act_res      `thenM` \ co_fn_res ->
 520     newUnique                                   `thenM` \ uniq ->
 521     let
 522         -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
 523         -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
 524         -- co_fn     :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
 525         arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
 526         coercion | isIdCoercion co_fn_arg,
 527                    isIdCoercion co_fn_res = idCoercion
 528                  | otherwise              = mkCoercion co_fn
 529
 530         co_fn e = DictLam [arg_id]
 531                      (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
 532                 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
 533                 --      HsVar arg_id :: HsExpr exp_arg
 534                 --      co_fn_arg $it :: HsExpr act_arg
 535                 --      HsApp e $it   :: HsExpr act_res
 536                 --      co_fn_res $it :: HsExpr exp_res
 537     in
 538     returnM coercion
 539 \end{code}
 540
 541
 542 %************************************************************************
 543 %*                                                                      *
 544 \subsection{Generalisation}
 545 %*                                                                      *
 546 %************************************************************************
 547
 548 \begin{code}
 549 tcGen :: TcSigmaType                            -- expected_ty
 550       -> TcTyVarSet                             -- Extra tyvars that the universally
 551                                                 --      quantified tyvars of expected_ty
 552                                                 --      must not be unified
 553       -> (TcRhoType -> TcM result)              -- spec_ty
 554       -> TcM (ExprCoFn, result)
 555         -- The expression has type: spec_ty -> expected_ty
 556
 557 tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
 558                                                 -- If not, the call is a no-op
 559   = do  {       -- We want the GenSkol info in the skolemised type variables to
 560                 -- mention the *instantiated* tyvar names, so that we get a
 561                 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
 562                 -- Hence the tiresome but innocuous fixM
 563           ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
 564                 do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
 565                    ; span <- getSrcSpanM
 566                    ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
 567                    ; return ((forall_tvs, theta, rho_ty), skol_info) })
 568
 569 #ifdef DEBUG
 570         ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
 571                                     text "expected_ty" <+> ppr expected_ty,
 572                                     text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
 573                                     text "free_tvs" <+> ppr free_tvs,
 574                                     text "forall_tvs" <+> ppr forall_tvs])
 575 #endif
 576
 577         -- Type-check the arg and unify with poly type
 578         ; (result, lie) <- getLIE (thing_inside rho_ty)
 579
 580         -- Check that the "forall_tvs" havn't been constrained
 581         -- The interesting bit here is that we must include the free variables
 582         -- of the expected_ty.  Here's an example:
 583         --       runST (newVar True)
 584         -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
 585         -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
 586         -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
 587         -- So now s' isn't unconstrained because it's linked to a.
 588         -- Conclusion: include the free vars of the expected_ty in the
 589         -- list of "free vars" for the signature check.
 590
 591         ; dicts <- newDicts (SigOrigin skol_info) theta
 592         ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
 593
 594         ; checkSigTyVarsWrt free_tvs forall_tvs
 595         ; traceTc (text "tcGen:done")
 596
 597         ; let
 598             -- This HsLet binds any Insts which came out of the simplification.
 599             -- It's a bit out of place here, but using AbsBind involves inventing
 600             -- a couple of new names which seems worse.
 601                 dict_ids = map instToId dicts
 602                 co_fn e  = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
 603         ; returnM (mkCoercion co_fn, result) }
 604   where
 605     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
 606     sig_msg  = ptext SLIT("expected type of an expression")
 607 \end{code}
 608
 609
 610
 611 %************************************************************************
 612 %*                                                                      *
 613 \subsection[Unify-exported]{Exported unification functions}
 614 %*                                                                      *
 615 %************************************************************************
 616
 617 The exported functions are all defined as versions of some
 618 non-exported generic functions.
 619
 620 Unify two @TauType@s.  Dead straightforward.
 621
 622 \begin{code}
 623 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 624 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
 625   =     -- The unifier should only ever see tau-types
 626         -- (no quantification whatsoever)
 627     ASSERT2( isTauTy ty1, ppr ty1 )
 628     ASSERT2( isTauTy ty2, ppr ty2 )
 629     addErrCtxtM (unifyCtxt "type" ty1 ty2) $
 630     uTys True ty1 ty1 True ty2 ty2
 631
 632 unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
 633 unifyTheta theta1 theta2
 634   = do { checkTc (equalLength theta1 theta2)
 635                  (ptext SLIT("Contexts differ in length"))
 636        ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
 637 \end{code}
 638
 639 @unifyTauTyList@ unifies corresponding elements of two lists of
 640 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
 641 of equal length.  We charge down the list explicitly so that we can
 642 complain if their lengths differ.
 643
 644 \begin{code}
 645 unifyTauTyLists :: Bool ->  -- Allow refinements on tys1
 646                    [TcTauType] ->
 647                    Bool ->  -- Allow refinements on tys2
 648                    [TcTauType] ->  TcM ()
 649 -- Precondition: lists must be same length
 650 -- Having the caller check gives better error messages
 651 -- Actually the caller neve does  need to check; see Note [Tycon app]
 652 unifyTauTyLists r1 []         r2 []             = returnM ()
 653 unifyTauTyLists r1 (ty1:tys1) r2 (ty2:tys2)     = uTys r1 ty1 ty1 r2 ty2 ty2   `thenM_`
 654                                         unifyTauTyLists r1 tys1 r2 tys2
 655 unifyTauTyLists r1 ty1s r2 ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 656 \end{code}
 657
 658 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 659 all together.  It is used, for example, when typechecking explicit
 660 lists, when all the elts should be of the same type.
 661
 662 \begin{code}
 663 unifyTauTyList :: [TcTauType] -> TcM ()
 664 unifyTauTyList []                = returnM ()
 665 unifyTauTyList [ty]              = returnM ()
 666 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenM_`
 667                                    unifyTauTyList tys
 668 \end{code}
 669
 670 %************************************************************************
 671 %*                                                                      *
 672 \subsection[Unify-uTys]{@uTys@: getting down to business}
 673 %*                                                                      *
 674 %************************************************************************
 675
 676 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 677 we want to report errors in terms of synomyms if poss.  The first of
 678 the pair is used in error messages only; it is always the same as the
 679 second, except that if the first is a synonym then the second may be a
 680 de-synonym'd version.  This way we get better error messages.
 681
 682 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 683
 684 \begin{code}
 685 uTys :: Bool                    -- Allow refinements to ty1
 686      -> TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 687                                 -- ty1 is the *expected* type
 688      -> Bool                    -- Allow refinements to ty2
 689      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 690                                 -- ty2 is the *actual* type
 691      -> TcM ()
 692
 693         -- Always expand synonyms (see notes at end)
 694         -- (this also throws away FTVs)
 695 uTys r1 ps_ty1 (NoteTy n1 ty1) r2 ps_ty2 ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
 696 uTys r1 ps_ty1 ty1 r2 ps_ty2 (NoteTy n2 ty2) = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
 697
 698         -- Variables; go for uVar
 699 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
 700 uTys r1 ps_ty1 ty1 r2 ps_ty2 (TyVarTy tyvar2) = uVar True  r2 tyvar2 r1 ps_ty1 ty1
 701                                         -- "True" means args swapped
 702
 703         -- Predicates
 704 uTys r1 _ (PredTy (IParam n1 t1)) r2 _ (PredTy (IParam n2 t2))
 705   | n1 == n2 = uTys r1 t1 t1 r2 t2 t2
 706 uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2))
 707   | c1 == c2 = unifyTauTyLists r1 tys1 r2 tys2
 708         -- Guaranteed equal lengths because the kinds check
 709
 710         -- Functions; just check the two parts
 711 uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2)
 712   = uTys r1 fun1 fun1 r2 fun2 fun2      `thenM_`    uTys r1 arg1 arg1 r2 arg2 arg2
 713
 714         -- Type constructors must match
 715 uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2)
 716   | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2
 717         -- See Note [TyCon app]
 718
 719         -- Applications need a bit of care!
 720         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 721         -- NB: we've already dealt with type variables and Notes,
 722         -- so if one type is an App the other one jolly well better be too
 723 uTys r1 ps_ty1 (AppTy s1 t1) r2 ps_ty2 ty2
 724   = case tcSplitAppTy_maybe ty2 of
 725         Just (s2,t2) -> uTys r1 s1 s1 r2 s2 s2  `thenM_`    uTys r1 t1 t1 r2 t2 t2
 726         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 727
 728         -- Now the same, but the other way round
 729         -- Don't swap the types, because the error messages get worse
 730 uTys r1 ps_ty1 ty1 r2 ps_ty2 (AppTy s2 t2)
 731   = case tcSplitAppTy_maybe ty1 of
 732         Just (s1,t1) -> uTys r1 s1 s1 r2 s2 s2  `thenM_`    uTys r1 t1 t1 r2 t2 t2
 733         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 734
 735         -- Not expecting for-alls in unification
 736         -- ... but the error message from the unifyMisMatch more informative
 737         -- than a panic message!
 738
 739         -- Anything else fails
 740 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 741 \end{code}
 742
 743 Note [Tycon app]
 744 ~~~~~~~~~~~~~~~~
 745 When we find two TyConApps, the argument lists are guaranteed equal
 746 length.  Reason: intially the kinds of the two types to be unified is
 747 the same. The only way it can become not the same is when unifying two
 748 AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
 749 the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
 750 which we do, that ensures that f1,f2 have the same kind; and that
 751 means a1,a2 have the same kind.  And now the argument repeats.
 752
 753
 754 Notes on synonyms
 755 ~~~~~~~~~~~~~~~~~
 756 If you are tempted to make a short cut on synonyms, as in this
 757 pseudocode...
 758
 759 \begin{verbatim}
 760 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 761 -- NO     = if (con1 == con2) then
 762 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
 763 -- NO   -- by unifying their arguments and ignoring their expansions.
 764 -- NO   unifyTauTypeLists args1 args2
 765 -- NO    else
 766 -- NO   -- Never mind.  Just expand them and try again
 767 -- NO   uTys ty1 ty2
 768 \end{verbatim}
 769
 770 then THINK AGAIN.  Here is the whole story, as detected and reported
 771 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 772 \begin{quotation}
 773 Here's a test program that should detect the problem:
 774
 775 \begin{verbatim}
 776         type Bogus a = Int
 777         x = (1 :: Bogus Char) :: Bogus Bool
 778 \end{verbatim}
 779
 780 The problem with [the attempted shortcut code] is that
 781 \begin{verbatim}
 782         con1 == con2
 783 \end{verbatim}
 784 is not a sufficient condition to be able to use the shortcut!
 785 You also need to know that the type synonym actually USES all
 786 its arguments.  For example, consider the following type synonym
 787 which does not use all its arguments.
 788 \begin{verbatim}
 789         type Bogus a = Int
 790 \end{verbatim}
 791
 792 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 793 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 794 would fail, even though the expanded forms (both \tr{Int}) should
 795 match.
 796
 797 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 798 unnecessarily bind \tr{t} to \tr{Char}.
 799
 800 ... You could explicitly test for the problem synonyms and mark them
 801 somehow as needing expansion, perhaps also issuing a warning to the
 802 user.
 803 \end{quotation}
 804
 805
 806 %************************************************************************
 807 %*                                                                      *
 808 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 809 %*                                                                      *
 810 %************************************************************************
 811
 812 @uVar@ is called when at least one of the types being unified is a
 813 variable.  It does {\em not} assume that the variable is a fixed point
 814 of the substitution; rather, notice that @uVar@ (defined below) nips
 815 back into @uTys@ if it turns out that the variable is already bound.
 816
 817 \begin{code}
 818 uVar :: Bool            -- False => tyvar is the "expected"
 819                         -- True  => ty    is the "expected" thing
 820      -> Bool            -- True, allow refinements to tv1, False don't
 821      -> TcTyVar
 822      -> Bool            -- Allow refinements to ty2?
 823      -> TcTauType -> TcTauType  -- printing and real versions
 824      -> TcM ()
 825
 826 uVar swapped r1 tv1 r2 ps_ty2 ty2
 827   = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2))       `thenM_`
 828     condLookupTcTyVar r1 tv1    `thenM` \ details ->
 829     case details of
 830         IndirectTv r1' ty1 | swapped   -> uTys r2   ps_ty2 ty2 r1' ty1    ty1   -- Swap back
 831                            | otherwise -> uTys r1' ty1     ty1 r2  ps_ty2 ty2   -- Same order
 832         DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
 833
 834 ----------------
 835 uDoneVar :: Bool                        -- Args are swapped
 836          -> TcTyVar -> TcTyVarDetails   -- Tyvar 1
 837          -> Bool                        -- Allow refinements to ty2
 838          -> TcTauType -> TcTauType      -- Type 2
 839          -> TcM ()
 840 -- Invariant: tyvar 1 is not unified with anything
 841
 842 uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
 843   =     -- Expand synonyms; ignore FTVs
 844     uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
 845
 846 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
 847         -- Same type variable => no-op
 848   | tv1 == tv2
 849   = returnM ()
 850
 851         -- Distinct type variables
 852   | otherwise
 853   = do  { lookup2 <- condLookupTcTyVar r2 tv2
 854         ; case lookup2 of
 855                 IndirectTv b ty2' -> uDoneVar  swapped tv1 details1 b ty2' ty2'
 856                 DoneTv details2   -> uDoneVars swapped tv1 details1 tv2 details2
 857         }
 858
 859 uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2     -- ty2 is not a type variable
 860   = case details1 of
 861         MetaTv ref1 -> do {     -- Do the occurs check, and check that we are not
 862                                 -- unifying a type variable with a polytype
 863                                 -- Returns a zonked type ready for the update
 864                             ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
 865                           ; updateMeta swapped tv1 ref1 ty2 }
 866
 867         skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
 868
 869
 870 ----------------
 871 uDoneVars :: Bool                       -- Args are swapped
 872           -> TcTyVar -> TcTyVarDetails  -- Tyvar 1
 873           -> TcTyVar -> TcTyVarDetails  -- Tyvar 2
 874           -> TcM ()
 875 -- Invarant: the type variables are distinct,
 876 -- and are not already unified with anything
 877
 878 uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
 879   = case details2 of
 880         MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 881         other                    -> updateMeta swapped       tv1 ref1 (mkTyVarTy tv2)
 882         -- Note that updateMeta does a sub-kind check
 883         -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
 884   where
 885     k1 = tyVarKind tv1
 886     k2 = tyVarKind tv2
 887     update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
 888         -- Update the variable with least kind info
 889         -- See notes on type inference in Kind.lhs
 890         -- The "nicer to" part only applies if the two kinds are the same,
 891         -- so we can choose which to do.
 892
 893     nicer_to_update_tv2 = isSystemName (varName tv2)
 894         -- Try to update sys-y type variables in preference to ones
 895         -- gotten (say) by instantiating a polymorphic function with
 896         -- a user-written type sig
 897
 898 uDoneVars swapped tv1 (SkolemTv _) tv2 details2
 899   = case details2 of
 900         MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 901         other       -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
 902
 903 uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
 904   = case details2 of
 905         MetaTv ref2   -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 906         SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
 907         other         -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
 908
 909 ----------------
 910 updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 911 -- Update tv1, which is flexi; occurs check is alrady done
 912 updateMeta swapped tv1 ref1 ty2
 913   = do  { checkKinds swapped tv1 ty2
 914         ; writeMutVar ref1 (Indirect ty2) }
 915 \end{code}
 916
 917 \begin{code}
 918 checkKinds swapped tv1 ty2
 919 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 920 -- ty2 has been zonked at this stage, which ensures that
 921 -- its kind has as much boxity information visible as possible.
 922   | tk2 `isSubKind` tk1 = returnM ()
 923
 924   | otherwise
 925         -- Either the kinds aren't compatible
 926         --      (can happen if we unify (a b) with (c d))
 927         -- or we are unifying a lifted type variable with an
 928         --      unlifted type: e.g.  (id 3#) is illegal
 929   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
 930     unifyKindMisMatch k1 k2
 931   where
 932     (k1,k2) | swapped   = (tk2,tk1)
 933             | otherwise = (tk1,tk2)
 934     tk1 = tyVarKind tv1
 935     tk2 = typeKind ty2
 936 \end{code}
 937
 938 \begin{code}
 939 checkValue tv1 r2 ps_ty2 non_var_ty2
 940 -- Do the occurs check, and check that we are not
 941 -- unifying a type variable with a polytype
 942 -- Return the type to update the type variable with, or fail
 943
 944 -- Basically we want to update     tv1 := ps_ty2
 945 -- because ps_ty2 has type-synonym info, which improves later error messages
 946 --
 947 -- But consider
 948 --      type A a = ()
 949 --
 950 --      f :: (A a -> a -> ()) -> ()
 951 --      f = \ _ -> ()
 952 --
 953 --      x :: ()
 954 --      x = f (\ x p -> p x)
 955 --
 956 -- In the application (p x), we try to match "t" with "A t".  If we go
 957 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
 958 -- an infinite loop later.
 959 -- But we should not reject the program, because A t = ().
 960 -- Rather, we should bind t to () (= non_var_ty2).
 961 --
 962 -- That's why we have this two-state occurs-check
 963   = zonk_tc_type r2 ps_ty2                      `thenM` \ ps_ty2' ->
 964     case okToUnifyWith tv1 ps_ty2' of {
 965         Nothing -> returnM ps_ty2' ;    -- Success
 966         other ->
 967
 968     zonk_tc_type r2 non_var_ty2         `thenM` \ non_var_ty2' ->
 969     case okToUnifyWith tv1 non_var_ty2' of
 970         Nothing ->      -- This branch rarely succeeds, except in strange cases
 971                         -- like that in the example above
 972                     returnM non_var_ty2'
 973
 974         Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
 975     }
 976   where
 977     zonk_tc_type refine ty
 978       = zonkType (\tv -> return (TyVarTy tv)) refine ty
 979         -- We may already be inside a wobbly type t2, and
 980         -- should take that into account here
 981
 982 data Problem = OccurCheck | NotMonoType
 983
 984 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
 985 -- (okToUnifyWith tv ty) checks whether it's ok to unify
 986 --      tv :=: ty
 987 -- Nothing => ok
 988 -- Just p  => not ok, problem p
 989
 990 okToUnifyWith tv ty
 991   = ok ty
 992   where
 993     ok (TyVarTy tv') | tv == tv' = Just OccurCheck
 994                      | otherwise = Nothing
 995     ok (AppTy t1 t2)            = ok t1 `and` ok t2
 996     ok (FunTy t1 t2)            = ok t1 `and` ok t2
 997     ok (TyConApp _ ts)          = oks ts
 998     ok (ForAllTy _ _)           = Just NotMonoType
 999     ok (PredTy st)              = ok_st st
1000     ok (NoteTy (FTVNote _) t)   = ok t
1001     ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
1002                 -- Type variables may be free in t1 but not t2
1003                 -- A forall may be in t2 but not t1
1004
1005     oks ts = foldr (and . ok) Nothing ts
1006
1007     ok_st (ClassP _ ts) = oks ts
1008     ok_st (IParam _ t)  = ok t
1009
1010     Nothing `and` m = m
1011     Just p  `and` m = Just p
1012 \end{code}
1013
1014
1015 %************************************************************************
1016 %*                                                                      *
1017                 Kind unification
1018 %*                                                                      *
1019 %************************************************************************
1020
1021 Unifying kinds is much, much simpler than unifying types.
1022
1023 \begin{code}
1024 unifyKind :: TcKind                 -- Expected
1025           -> TcKind                 -- Actual
1026           -> TcM ()
1027 unifyKind LiftedTypeKind   LiftedTypeKind   = returnM ()
1028 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
1029
1030 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
1031 unifyKind ArgTypeKind  k2 | isArgTypeKind k2    = returnM ()
1032   -- Respect sub-kinding
1033
1034 unifyKind (FunKind a1 r1) (FunKind a2 r2)
1035  = do { unifyKind a2 a1; unifyKind r1 r2 }
1036                 -- Notice the flip in the argument,
1037                 -- so that the sub-kinding works right
1038
1039 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
1040 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
1041 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1042
1043 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1044 unifyKinds []       []       = returnM ()
1045 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenM_`
1046                                unifyKinds ks1 ks2
1047 unifyKinds _ _               = panic "unifyKinds: length mis-match"
1048
1049 ----------------
1050 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1051 uKVar swapped kv1 k2
1052   = do  { mb_k1 <- readKindVar kv1
1053         ; case mb_k1 of
1054             Nothing -> uUnboundKVar swapped kv1 k2
1055             Just k1 | swapped   -> unifyKind k2 k1
1056                     | otherwise -> unifyKind k1 k2 }
1057
1058 ----------------
1059 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1060 uUnboundKVar swapped kv1 k2@(KindVar kv2)
1061   | kv1 == kv2 = returnM ()
1062   | otherwise   -- Distinct kind variables
1063   = do  { mb_k2 <- readKindVar kv2
1064         ; case mb_k2 of
1065             Just k2 -> uUnboundKVar swapped kv1 k2
1066             Nothing -> writeKindVar kv1 k2 }
1067
1068 uUnboundKVar swapped kv1 non_var_k2
1069   = do  { k2' <- zonkTcKind non_var_k2
1070         ; kindOccurCheck kv1 k2'
1071         ; k2'' <- kindSimpleKind swapped k2'
1072                 -- KindVars must be bound only to simple kinds
1073                 -- Polarities: (kindSimpleKind True ?) succeeds
1074                 -- returning *, corresponding to unifying
1075                 --      expected: ?
1076                 --      actual:   kind-ver
1077         ; writeKindVar kv1 k2'' }
1078
1079 ----------------
1080 kindOccurCheck kv1 k2   -- k2 is zonked
1081   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1082   where
1083     not_in (KindVar kv2)   = kv1 /= kv2
1084     not_in (FunKind a2 r2) = not_in a2 && not_in r2
1085     not_in other           = True
1086
1087 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1088 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1089 -- If the flag is False, it requires k <: sk
1090 -- E.g.         kindSimpleKind False ?? = *
1091 -- What about (kv -> *) :=: ?? -> *
1092 kindSimpleKind orig_swapped orig_kind
1093   = go orig_swapped orig_kind
1094   where
1095     go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
1096                                ; k2' <- go sw k2
1097                                ; return (FunKind k1' k2') }
1098     go True OpenTypeKind = return liftedTypeKind
1099     go True ArgTypeKind  = return liftedTypeKind
1100     go sw LiftedTypeKind  = return liftedTypeKind
1101     go sw k@(KindVar _)   = return k    -- KindVars are always simple
1102     go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1103                                   <+> ppr orig_swapped <+> ppr orig_kind)
1104         -- I think this can't actually happen
1105
1106 -- T v = MkT v           v must be a type
1107 -- T v w = MkT (v -> w)  v must not be an umboxed tuple
1108
1109 ----------------
1110 kindOccurCheckErr tyvar ty
1111   = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1112        2 (sep [ppr tyvar, char '=', ppr ty])
1113
1114 unifyKindMisMatch ty1 ty2
1115   = zonkTcKind ty1      `thenM` \ ty1' ->
1116     zonkTcKind ty2      `thenM` \ ty2' ->
1117     let
1118         msg = hang (ptext SLIT("Couldn't match kind"))
1119                    2 (sep [quotes (ppr ty1'),
1120                            ptext SLIT("against"),
1121                            quotes (ppr ty2')])
1122     in
1123     failWithTc msg
1124 \end{code}
1125
1126 \begin{code}
1127 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1128 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1129
1130 unifyFunKind (KindVar kvar)
1131   = readKindVar kvar    `thenM` \ maybe_kind ->
1132     case maybe_kind of
1133         Just fun_kind -> unifyFunKind fun_kind
1134         Nothing       -> do { arg_kind <- newKindVar
1135                             ; res_kind <- newKindVar
1136                             ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1137                             ; returnM (Just (arg_kind,res_kind)) }
1138
1139 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1140 unifyFunKind other                       = returnM Nothing
1141 \end{code}
1142
1143 %************************************************************************
1144 %*                                                                      *
1145 \subsection[Unify-context]{Errors and contexts}
1146 %*                                                                      *
1147 %************************************************************************
1148
1149 Errors
1150 ~~~~~~
1151
1152 \begin{code}
1153 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
1154   = zonkTcType ty1      `thenM` \ ty1' ->
1155     zonkTcType ty2      `thenM` \ ty2' ->
1156     returnM (err ty1' ty2')
1157   where
1158     err ty1 ty2 = (env1,
1159                    nest 2
1160                         (vcat [
1161                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1162                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1163                         ]))
1164                   where
1165                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1166
1167 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
1168         -- tv1 and ty2 are zonked already
1169   = returnM msg
1170   where
1171     msg = (env2, ptext SLIT("When matching the kinds of") <+>
1172                  sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1173
1174     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
1175                              | otherwise = (pp1, pp2)
1176     (env1, tv1') = tidyOpenTyVar tidy_env tv1
1177     (env2, ty2') = tidyOpenType  env1 ty2
1178     pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1179     pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1180
1181 unifyMisMatch ty1 ty2
1182   = do  { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
1183         ; (env2, pp2, extra2) <- ppr_ty env1 ty2
1184         ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)],
1185                          nest 2 extra1, nest 2 extra2]
1186     in
1187     failWithTcM (env2, msg) }
1188
1189 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1190 ppr_ty env ty
1191   = do { ty' <- zonkTcType ty
1192        ; let (env1,tidy_ty) = tidyOpenType env ty'
1193              simple_result  = (env1, quotes (ppr tidy_ty), empty)
1194        ; case tidy_ty of
1195            TyVarTy tv
1196                 | isSkolemTyVar tv -> return (env2, pp_rigid tv',
1197                                               pprTcTyVar tv')
1198                 | otherwise -> return simple_result
1199                 where
1200                   (env2, tv') = tidySkolemTyVar env1 tv
1201            other -> return simple_result }
1202   where
1203     pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
1204
1205 unifyCheck problem tyvar ty
1206   = (env2, hang msg
1207               2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1208   where
1209     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1210     (env2, tidy_ty)    = tidyOpenType  env1         ty
1211
1212     msg = case problem of
1213             OccurCheck  -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1214             NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1215 \end{code}
1216
1217
1218 %************************************************************************
1219 %*                                                                      *
1220         Checking kinds
1221 %*                                                                      *
1222 %************************************************************************
1223
1224 ---------------------------
1225 -- We would like to get a decent error message from
1226 --   (a) Under-applied type constructors
1227 --              f :: (Maybe, Maybe)
1228 --   (b) Over-applied type constructors
1229 --              f :: Int x -> Int x
1230 --
1231
1232 \begin{code}
1233 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1234 -- A fancy wrapper for 'unifyKind', which tries
1235 -- to give decent error messages.
1236 checkExpectedKind ty act_kind exp_kind
1237   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1238   = returnM ()
1239   | otherwise
1240   = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
1241     case mb_r of {
1242         Just _  -> returnM () ; -- Unification succeeded
1243         Nothing ->
1244
1245         -- So there's definitely an error
1246         -- Now to find out what sort
1247     zonkTcKind exp_kind         `thenM` \ exp_kind ->
1248     zonkTcKind act_kind         `thenM` \ act_kind ->
1249
1250     let (exp_as, _) = splitKindFunTys exp_kind
1251         (act_as, _) = splitKindFunTys act_kind
1252         n_exp_as = length exp_as
1253         n_act_as = length act_as
1254
1255         err | n_exp_as < n_act_as       -- E.g. [Maybe]
1256             = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1257
1258                 -- Now n_exp_as >= n_act_as. In the next two cases,
1259                 -- n_exp_as == 0, and hence so is n_act_as
1260             | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1261             = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1262                 <+> ptext SLIT("is unlifted")
1263
1264             | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1265             = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1266                 <+> ptext SLIT("is lifted")
1267
1268             | otherwise                 -- E.g. Monad [Int]
1269             = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
1270                     ptext SLIT("but") <+> quotes (ppr ty) <+>
1271                     ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
1272    in
1273    failWithTc (ptext SLIT("Kind error:") <+> err)
1274    }
1275 \end{code}
1276
1277 %************************************************************************
1278 %*                                                                      *
1279 \subsection{Checking signature type variables}
1280 %*                                                                      *
1281 %************************************************************************
1282
1283 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1284 are not mentioned in the environment.  In particular:
1285
1286         (a) Not mentioned in the type of a variable in the envt
1287                 eg the signature for f in this:
1288
1289                         g x = ... where
1290                                         f :: a->[a]
1291                                         f y = [x,y]
1292
1293                 Here, f is forced to be monorphic by the free occurence of x.
1294
1295         (d) Not (unified with another type variable that is) in scope.
1296                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1297             when checking the expression type signature, we find that
1298             even though there is nothing in scope whose type mentions r,
1299             nevertheless the type signature for the expression isn't right.
1300
1301             Another example is in a class or instance declaration:
1302                 class C a where
1303                    op :: forall b. a -> b
1304                    op x = x
1305             Here, b gets unified with a
1306
1307 Before doing this, the substitution is applied to the signature type variable.
1308
1309 \begin{code}
1310 checkSigTyVars :: [TcTyVar] -> TcM ()
1311 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1312
1313 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1314 checkSigTyVarsWrt extra_tvs sig_tvs
1315   = zonkTcTyVarsAndFV (varSetElems extra_tvs)   `thenM` \ extra_tvs' ->
1316     check_sig_tyvars extra_tvs' sig_tvs
1317
1318 check_sig_tyvars
1319         :: TcTyVarSet   -- Global type variables. The universally quantified
1320                         --      tyvars should not mention any of these
1321                         --      Guaranteed already zonked.
1322         -> [TcTyVar]    -- Universally-quantified type variables in the signature
1323                         --      Guaranteed to be skolems
1324         -> TcM ()
1325 check_sig_tyvars extra_tvs []
1326   = returnM ()
1327 check_sig_tyvars extra_tvs sig_tvs
1328   = ASSERT( all isSkolemTyVar sig_tvs )
1329     do  { gbl_tvs <- tcGetGlobalTyVars
1330         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1331                                       text "gbl_tvs" <+> ppr gbl_tvs,
1332                                       text "extra_tvs" <+> ppr extra_tvs]))
1333
1334         ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1335         ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
1336               (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1337         }
1338
1339 bleatEscapedTvs :: TcTyVarSet   -- The global tvs
1340                 -> [TcTyVar]    -- The possibly-escaping type variables
1341                 -> [TcTyVar]    -- The zonked versions thereof
1342                 -> TcM ()
1343 -- Complain about escaping type variables
1344 -- We pass a list of type variables, at least one of which
1345 -- escapes.  The first list contains the original signature type variable,
1346 -- while the second  contains the type variable it is unified to (usually itself)
1347 bleatEscapedTvs globals sig_tvs zonked_tvs
1348   = do  { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1349         ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1350   where
1351     (env1, tidy_tvs)         = tidyOpenTyVars emptyTidyEnv sig_tvs
1352     (env2, tidy_zonked_tvs) = tidyOpenTyVars env1         zonked_tvs
1353
1354     main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1355
1356     check (tidy_env, msgs) (sig_tv, zonked_tv)
1357       | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1358       | otherwise
1359       = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
1360            ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1361
1362 -----------------------
1363 escape_msg sig_tv zonked_tv globs
1364   | notNull globs
1365   = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
1366           nest 2 (vcat globs)]
1367   | otherwise
1368   = msg <+> ptext SLIT("escapes")
1369         -- Sigh.  It's really hard to give a good error message
1370         -- all the time.   One bad case is an existential pattern match.
1371         -- We rely on the "When..." context to help.
1372   where
1373     msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1374     is_bound_to
1375         | sig_tv == zonked_tv = empty
1376         | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
1377 \end{code}
1378
1379 These two context are used with checkSigTyVars
1380
1381 \begin{code}
1382 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1383         -> TidyEnv -> TcM (TidyEnv, Message)
1384 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1385   = zonkTcType sig_tau          `thenM` \ actual_tau ->
1386     let
1387         (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
1388         (env2, tidy_sig_rho)    = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1389         (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1390         sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1391                         ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1392                    ]
1393         msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
1394                     nest 2 sub_msg]
1395     in
1396     returnM (env3, msg)
1397 \end{code}