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