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