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