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