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