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