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