ghc/compiler/typecheck/TcUnify.lhs

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