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   tcSubPat, tcSubExp, tcSub, tcGen,
  10   checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
  11
  12         -- Various unifications
  13   unifyTauTy, unifyTauTyList, unifyTheta,
  14   unifyKind, unifyKinds, unifyFunKind,
  15   checkExpectedKind,
  16
  17   --------------------------------
  18   -- Holes
  19   Expected(..), tcInfer, readExpectedType,
  20   zapExpectedType, zapExpectedTo, zapExpectedBranches,
  21   subFunTys,     unifyFunTys,
  22   zapToListTy,   unifyListTy,
  23   zapToTyConApp, unifyTyConApp,
  24   unifyAppTy
  25   ) where
  26
  27 #include "HsVersions.h"
  28
  29 import HsSyn            ( HsExpr(..) , MatchGroup(..), HsMatchContext(..),
  30                           hsLMatchPats, pprMatches, pprMatchContext )
  31 import TcHsSyn          ( mkHsDictLet, mkHsDictLam,
  32                           ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
  33 import TypeRep          ( Type(..), PredType(..), TyNote(..) )
  34
  35 import TcRnMonad         -- TcType, amongst others
  36 import TcType           ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
  37                           TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
  38                           SkolemInfo( GenSkol ), MetaDetails(..),
  39                           pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp,
  40                           tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType,
  41                           tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
  42                           typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
  43                           tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
  44                           pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar )
  45 import Kind             ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
  46                           openTypeKind, liftedTypeKind, mkArrowKind,
  47                           isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
  48                           isSubKind, pprKind, splitKindFunTys )
  49 import Inst             ( newDicts, instToId, tcInstCall )
  50 import TcMType          ( condLookupTcTyVar, LookupTyVarResult(..),
  51                           tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
  52                           newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV,
  53                           readKindVar, writeKindVar )
  54 import TcSimplify       ( tcSimplifyCheck )
  55 import TcIface          ( checkWiredInTyCon )
  56 import TcEnv            ( tcGetGlobalTyVars, findGlobals )
  57 import TyCon            ( TyCon, tyConArity, tyConTyVars )
  58 import TysWiredIn       ( listTyCon )
  59 import Id               ( Id, mkSysLocal )
  60 import Var              ( Var, varName, tyVarKind )
  61 import VarSet           ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
  62 import VarEnv
  63 import Name             ( Name, isSystemName, mkSysTvName )
  64 import ErrUtils         ( Message )
  65 import SrcLoc           ( noLoc )
  66 import BasicTypes       ( Arity )
  67 import Util             ( notNull, equalLength )
  68 import Outputable
  69 \end{code}
  70
  71 Notes on holes
  72 ~~~~~~~~~~~~~~
  73 * A hole is always filled in with an ordinary type, not another hole.
  74
  75 %************************************************************************
  76 %*                                                                      *
  77 \subsection{'hole' type variables}
  78 %*                                                                      *
  79 %************************************************************************
  80
  81 \begin{code}
  82 newHole = newMutVar (error "Empty hole in typechecker")
  83
  84 tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
  85 tcInfer tc_infer
  86   = do  { hole <- newHole
  87         ; res <- tc_infer (Infer hole)
  88         ; res_ty <- readMutVar hole
  89         ; return (res, res_ty) }
  90
  91 readExpectedType :: Expected ty -> TcM ty
  92 readExpectedType (Infer hole) = readMutVar hole
  93 readExpectedType (Check ty)   = returnM ty
  94
  95 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
  96 -- In the inference case, ensure we have a monotype
  97 -- (including an unboxed tuple)
  98 zapExpectedType (Infer hole) kind
  99   = do { ty <- newTyFlexiVarTy kind ;
 100          writeMutVar hole ty ;
 101          return ty }
 102
 103 zapExpectedType (Check ty) kind
 104   | typeKind ty `isSubKind` kind = return ty
 105   | otherwise                    = do { ty1 <- newTyFlexiVarTy kind
 106                                       ; unifyTauTy ty1 ty
 107                                       ; return ty }
 108         -- The unify is to ensure that 'ty' has the desired kind
 109         -- For example, in (case e of r -> b) we push an OpenTypeKind
 110         -- type variable
 111
 112 zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
 113 -- If there is more than one branch in a case expression,
 114 -- and exp_ty is a 'hole', all branches must be types, not type schemes,
 115 -- otherwise the order in which we check them would affect the result.
 116 zapExpectedBranches (MatchGroup [match] _) exp_ty
 117    = return exp_ty      -- One branch
 118 zapExpectedBranches matches (Check ty)
 119   = return (Check ty)
 120 zapExpectedBranches matches (Infer hole)
 121   = do  {       -- Many branches, and inference mode,
 122                 -- so switch to checking mode with a monotype
 123           ty <- newTyFlexiVarTy openTypeKind
 124         ; writeMutVar hole ty
 125         ; return (Check ty) }
 126
 127 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
 128 zapExpectedTo (Check ty1)  ty2 = unifyTauTy ty1 ty2
 129 zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
 130         -- See Note [Zonk return type]
 131
 132 instance Outputable ty => Outputable (Expected ty) where
 133   ppr (Check ty)   = ptext SLIT("Expected type") <+> ppr ty
 134   ppr (Infer hole) = ptext SLIT("Inferring type")
 135 \end{code}
 136
 137
 138 %************************************************************************
 139 %*                                                                      *
 140 \subsection[Unify-fun]{@unifyFunTy@}
 141 %*                                                                      *
 142 %************************************************************************
 143
 144 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
 145 creation of type variables.
 146
 147 * subFunTy is used when we might be faced with a "hole" type variable,
 148   in which case we should create two new holes.
 149
 150 * unifyFunTy is used when we expect to encounter only "ordinary"
 151   type variables, so we should create new ordinary type variables
 152
 153 \begin{code}
 154 subFunTys :: HsMatchContext Name
 155           -> MatchGroup Name
 156           -> Expected TcRhoType         -- Fail if ty isn't a function type
 157           -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
 158           -> TcM a
 159
 160 subFunTys ctxt (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
 161   =     -- This is the interesting case
 162     ASSERT( null null_matches )
 163     do  { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
 164         ; res_hole  <- newHole
 165
 166                 -- Do the business
 167         ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
 168
 169                 -- Extract the answers
 170         ; arg_tys <- mapM readMutVar pat_holes
 171         ; res_ty  <- readMutVar res_hole
 172
 173                 -- Write the answer into the incoming hole
 174         ; writeMutVar hole (mkFunTys arg_tys res_ty)
 175
 176                 -- And return the answer
 177         ; return res }
 178
 179 subFunTys ctxt group@(MatchGroup (match:matches) _) (Check ty) thing_inside
 180   = ASSERT( all ((== n_pats) . length . hsLMatchPats) matches )
 181         -- Assertion just checks that all the matches have the same number of pats
 182     do  { (pat_tys, res_ty) <- unifyFunTys msg n_pats ty
 183         ; thing_inside (map Check pat_tys) (Check res_ty) }
 184   where
 185     n_pats = length (hsLMatchPats match)
 186     msg = case ctxt of
 187             FunRhs fun -> ptext SLIT("The equation(s) for") <+> quotes (ppr fun)
 188                           <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument"))
 189             LambdaExpr -> sep [ ptext SLIT("The lambda expression")
 190                                   <+> quotes (pprSetDepth 1 $ pprMatches ctxt group),
 191                                         -- The pprSetDepth makes the abstraction print briefly
 192                                 ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("arguments"))]
 193             other      -> pprPanic "subFunTys" (pprMatchContext ctxt)
 194
 195
 196 unifyFunTys :: SDoc -> Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
 197 -- Fail if ty isn't a function type, otherwise return arg and result types
 198 -- The result types are guaranteed wobbly if the argument is wobbly
 199 --
 200 -- Does not allocate unnecessary meta variables: if the input already is
 201 -- a function, we just take it apart.  Not only is this efficient, it's important
 202 -- for  (a) higher rank: the argument might be of form
 203 --              (forall a. ty) -> other
 204 --          If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
 205 --          blow up with the meta var meets the forall
 206 --
 207 --      (b) GADTs: if the argument is not wobbly we do not want the result to be
 208
 209 {-
 210         Error messages from unifyFunTys
 211         The first line is passed in as error_herald
 212
 213    The abstraction `\Just 1 -> ...' has two arguments
 214    but its type `Maybe a -> a' has only one
 215
 216    The equation(s) for `f' have two arguments
 217    but its type `Maybe a -> a' has only one
 218
 219    The section `(f 3)' requires 'f' to take two arguments
 220    but its type `Int -> Int' has only one
 221
 222    The function 'f' is applied to two arguments
 223    but its type `Int -> Int' has only one
 224 -}
 225
 226 unifyFunTys error_herald arity ty
 227         -- error_herald is the whole first line of the error message above
 228   = do  { (ok, args, res) <- unify_fun_ty True arity ty
 229         ; if ok then return (args, res)
 230           else failWithTc (mk_msg (length args)) }
 231   where
 232     mk_msg n_actual
 233       = error_herald <> comma $$
 234         sep [ptext SLIT("but its type") <+> quotes (pprType ty),
 235              if n_actual == 0 then ptext SLIT("has none")
 236              else ptext SLIT("has only") <+> speakN n_actual]
 237
 238 unify_fun_ty :: Bool -> Arity -> TcRhoType
 239              -> TcM (Bool,              -- Arity satisfied?
 240                      [TcSigmaType],     -- Arg types found; length <= arity
 241                      TcRhoType)         -- Result type
 242
 243 unify_fun_ty use_refinement arity ty
 244   | arity == 0
 245   = do  { res_ty <- wobblify use_refinement ty
 246         ; return (True, [], ty) }
 247
 248 unify_fun_ty use_refinement arity (NoteTy _ ty)
 249   = unify_fun_ty use_refinement arity ty
 250
 251 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
 252   = do  { details <- condLookupTcTyVar use_refinement tv
 253         ; case details of
 254             IndirectTv use' ty' -> unify_fun_ty use' arity ty'
 255             DoneTv (MetaTv ref) -> ASSERT( liftedTypeKind `isSubKind` tyVarKind tv )
 256                                         -- The argument to unifyFunTys is always a type
 257                                         -- Occurs check can't happen, of course
 258                                    do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
 259                                       ; res <- newTyFlexiVarTy openTypeKind
 260                                       ; writeMutVar ref (Indirect (mkFunTys args res))
 261                                       ; return (True, args, res) }
 262             DoneTv skol         -> return (False, [], ty)
 263         }
 264
 265 unify_fun_ty use_refinement arity ty
 266   | Just (arg,res) <- tcSplitFunTy_maybe ty
 267   = do  { arg' <- wobblify use_refinement arg
 268         ; (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
 269         ; return (ok, arg':args', res') }
 270
 271 unify_fun_ty use_refinement arity ty
 272 -- Common cases are all done by now
 273 -- At this point we usually have an error, but ty could
 274 -- be (a Int Bool), or (a Bool), which can match
 275 -- So just use the unifier.  But catch any error so we just
 276 -- return the success/fail boolean
 277   = do  { arg <- newTyFlexiVarTy argTypeKind
 278         ; res <- newTyFlexiVarTy openTypeKind
 279         ; let fun_ty = mkFunTy arg res
 280         ; (_, mb_unit) <- tryTc (uTys True ty ty True fun_ty fun_ty)
 281         ; case mb_unit of {
 282             Nothing -> return (False, [], ty) ;
 283             Just _  ->
 284     do { (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res
 285        ; return (ok, arg:args', res')
 286     } } }
 287 \end{code}
 288
 289 \begin{code}
 290 ----------------------
 291 zapToTyConApp :: TyCon                  -- T :: k1 -> ... -> kn -> *
 292               -> Expected TcSigmaType   -- Expected type (T a b c)
 293               -> TcM [TcType]           -- Element types, a b c
 294   -- Insists that the Expected type is not a forall-type
 295   -- It's used for wired-in tycons, so we call checkWiredInTyCOn
 296 zapToTyConApp tc (Check ty)
 297    = do { checkWiredInTyCon tc ; unifyTyConApp tc ty }   -- NB: fails for a forall-type
 298
 299 zapToTyConApp tc (Infer hole)
 300   = do  { (tc_app, elt_tys) <- newTyConApp tc
 301         ; writeMutVar hole tc_app
 302         ; traceTc (text "zap" <+> ppr tc)
 303         ; checkWiredInTyCon tc
 304         ; return elt_tys }
 305
 306 zapToListTy :: Expected TcType -> TcM TcType    -- Special case for lists
 307 zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
 308                         ; return elt_ty }
 309
 310 ----------------------
 311 unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
 312 unifyTyConApp tc ty = unify_tc_app True tc ty
 313         -- Add a boolean flag to remember whether to use
 314         -- the type refinement or not
 315
 316 unifyListTy :: TcType -> TcM TcType     -- Special case for lists
 317 unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
 318                         ; return elt_ty }
 319
 320 ----------
 321 unify_tc_app use_refinement tc (NoteTy _ ty)
 322   = unify_tc_app use_refinement tc ty
 323
 324 unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
 325   = do  { details <- condLookupTcTyVar use_refinement tyvar
 326         ; case details of
 327             IndirectTv use' ty' -> unify_tc_app use' tc ty'
 328             other               -> unify_tc_app_help tc ty
 329         }
 330
 331 unify_tc_app use_refinement tc ty
 332   | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
 333     tycon == tc
 334   = ASSERT( tyConArity tycon == length arg_tys )        -- ty::*
 335     mapM (wobblify use_refinement) arg_tys
 336
 337 unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
 338
 339 unify_tc_app_help tc ty         -- Revert to ordinary unification
 340   = do  { (tc_app, arg_tys) <- newTyConApp tc
 341         ; if not (isTauTy ty) then      -- Can happen if we call zapToTyConApp tc (forall a. ty)
 342              unifyMisMatch ty tc_app
 343           else do
 344         { unifyTauTy ty tc_app
 345         ; returnM arg_tys } }
 346
 347
 348 ----------------------
 349 unifyAppTy :: TcType                    -- Type to split: m a
 350            -> TcM (TcType, TcType)      -- (m,a)
 351 -- Assumes (m:*->*)
 352
 353 unifyAppTy ty = unify_app_ty True ty
 354
 355 unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty
 356
 357 unify_app_ty use ty@(TyVarTy tyvar)
 358   = do  { details <- condLookupTcTyVar use tyvar
 359         ; case details of
 360             IndirectTv use' ty' -> unify_app_ty use' ty'
 361             other               -> unify_app_ty_help ty
 362         }
 363
 364 unify_app_ty use ty
 365   | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
 366   = do  { fun' <- wobblify use fun_ty
 367         ; arg' <- wobblify use arg_ty
 368         ; return (fun', arg') }
 369
 370   | otherwise = unify_app_ty_help ty
 371
 372 unify_app_ty_help ty            -- Revert to ordinary unification
 373   = do  { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind)
 374         ; arg_ty <- newTyFlexiVarTy liftedTypeKind
 375         ; unifyTauTy (mkAppTy fun_ty arg_ty) ty
 376         ; return (fun_ty, arg_ty) }
 377
 378
 379 ----------------------
 380 wobblify :: Bool        -- True <=> don't wobblify
 381          -> TcTauType
 382          -> TcM TcTauType
 383 -- Return a wobbly type.  At the moment we do that by
 384 -- allocating a fresh meta type variable.
 385 wobblify True  ty = return ty
 386 wobblify False ty = do  { uniq <- newUnique
 387                         ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
 388                                              (typeKind ty)
 389                                              (Indirect ty)
 390                         ; return (mkTyVarTy tv) }
 391
 392 ----------------------
 393 newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
 394 newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
 395                     ; return (mkTyConApp tc args, args) }
 396 \end{code}
 397
 398
 399 %************************************************************************
 400 %*                                                                      *
 401 \subsection{Subsumption}
 402 %*                                                                      *
 403 %************************************************************************
 404
 405 All the tcSub calls have the form
 406
 407                 tcSub expected_ty offered_ty
 408 which checks
 409                 offered_ty <= expected_ty
 410
 411 That is, that a value of type offered_ty is acceptable in
 412 a place expecting a value of type expected_ty.
 413
 414 It returns a coercion function
 415         co_fn :: offered_ty -> expected_ty
 416 which takes an HsExpr of type offered_ty into one of type
 417 expected_ty.
 418
 419 \begin{code}
 420 -----------------------
 421 -- tcSubExp is used for expressions
 422 tcSubExp :: Expected TcRhoType -> TcRhoType  -> TcM ExprCoFn
 423
 424 tcSubExp (Infer hole) offered_ty
 425   = do { offered' <- zonkTcType offered_ty
 426         -- Note [Zonk return type]
 427         -- zonk to take advantage of the current GADT type refinement.
 428         -- If we don't we get spurious "existential type variable escapes":
 429         --      case (x::Maybe a) of
 430         --        Just b (y::b) -> y
 431         -- We need the refinement [b->a] to be applied to the result type
 432         ; writeMutVar hole offered'
 433         ; return idCoercion }
 434
 435 tcSubExp (Check expected_ty) offered_ty
 436   = tcSub expected_ty offered_ty
 437
 438 -----------------------
 439 -- tcSubPat is used for patterns
 440 tcSubPat :: TcSigmaType                 -- Pattern type signature
 441          -> Expected TcSigmaType        -- Type from context
 442          -> TcM ()
 443 -- In patterns we insist on an exact match; hence no CoFn returned
 444 --      See Note [Pattern coercions] in TcPat
 445 -- However, we can't call unify directly, because both types might be
 446 -- polymorphic; hence the call to tcSub, followed by a check for
 447 -- equal types.  (We can't just check for the identity coercion, because
 448 -- in the polymorphic case we might get back something eta-equivalent to
 449 -- the identity coercion, but that's not easy to tell.)
 450
 451 tcSubPat sig_ty (Infer hole)
 452   = do { sig_ty' <- zonkTcType sig_ty
 453         ; writeMutVar hole sig_ty'      -- See notes with tcSubExp above
 454         ; return () }
 455
 456 -- This tcSub followed by tcEqType checks for identical types
 457 -- It'd be done more neatly by augmenting the unifier to deal with
 458 -- (identically shaped) for-all types.
 459
 460 tcSubPat sig_ty (Check exp_ty)
 461   = do  { co_fn <- tcSub sig_ty exp_ty
 462         ; sig_ty' <- zonkTcType sig_ty
 463         ; exp_ty' <- zonkTcType exp_ty
 464         ; if tcEqType sig_ty' exp_ty' then
 465                 return ()
 466           else do
 467         { (env, msg) <- misMatchMsg sig_ty' exp_ty'
 468         ; failWithTcM (env, msg $$ extra) } }
 469   where
 470     extra | isTauTy sig_ty = empty
 471           | otherwise      = ptext SLIT("Polymorphic types must match exactly in patterns")
 472 \end{code}
 473
 474
 475
 476 %************************************************************************
 477 %*                                                                      *
 478         tcSub: main subsumption-check code
 479 %*                                                                      *
 480 %************************************************************************
 481
 482 No holes expected now.  Add some error-check context info.
 483
 484 \begin{code}
 485 -----------------
 486 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn     -- Locally used only
 487         -- tcSub exp act checks that
 488         --      act <= exp
 489 tcSub expected_ty actual_ty
 490   = traceTc (text "tcSub" <+> details)          `thenM_`
 491     addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
 492                 (tc_sub expected_ty expected_ty actual_ty actual_ty)
 493   where
 494     details = vcat [text "Expected:" <+> ppr expected_ty,
 495                     text "Actual:  " <+> ppr actual_ty]
 496
 497 -----------------
 498 tc_sub :: TcSigmaType           -- expected_ty, before expanding synonyms
 499        -> TcSigmaType           --              ..and after
 500        -> TcSigmaType           -- actual_ty, before
 501        -> TcSigmaType           --              ..and after
 502        -> TcM ExprCoFn
 503
 504 -----------------------------------
 505 -- Expand synonyms
 506 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
 507 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
 508
 509 -----------------------------------
 510 -- Generalisation case
 511 --      actual_ty:   d:Eq b => b->b
 512 --      expected_ty: forall a. Ord a => a->a
 513 --      co_fn e      /\a. \d2:Ord a. let d = eqFromOrd d2 in e
 514
 515 -- It is essential to do this *before* the specialisation case
 516 -- Example:  f :: (Eq a => a->a) -> ...
 517 --           g :: Ord b => b->b
 518 -- Consider  f g !
 519
 520 tc_sub exp_sty expected_ty act_sty actual_ty
 521   | isSigmaTy expected_ty
 522   = tcGen expected_ty (tyVarsOfType actual_ty) (
 523         -- It's really important to check for escape wrt the free vars of
 524         -- both expected_ty *and* actual_ty
 525         \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
 526     )                           `thenM` \ (gen_fn, co_fn) ->
 527     returnM (gen_fn <.> co_fn)
 528
 529 -----------------------------------
 530 -- Specialisation case:
 531 --      actual_ty:   forall a. Ord a => a->a
 532 --      expected_ty: Int -> Int
 533 --      co_fn e =    e Int dOrdInt
 534
 535 tc_sub exp_sty expected_ty act_sty actual_ty
 536   | isSigmaTy actual_ty
 537   = tcInstCall InstSigOrigin actual_ty          `thenM` \ (inst_fn, _, body_ty) ->
 538     tc_sub exp_sty expected_ty body_ty body_ty  `thenM` \ co_fn ->
 539     returnM (co_fn <.> inst_fn)
 540
 541 -----------------------------------
 542 -- Function case
 543
 544 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
 545   = tcSub_fun exp_arg exp_res act_arg act_res
 546
 547 -----------------------------------
 548 -- Type variable meets function: imitate
 549 --
 550 -- NB 1: we can't just unify the type variable with the type
 551 --       because the type might not be a tau-type, and we aren't
 552 --       allowed to instantiate an ordinary type variable with
 553 --       a sigma-type
 554 --
 555 -- NB 2: can we short-cut to an error case?
 556 --       when the arg/res is not a tau-type?
 557 -- NO!  e.g.   f :: ((forall a. a->a) -> Int) -> Int
 558 --      then   x = (f,f)
 559 --      is perfectly fine, because we can instantiate f's type to a monotype
 560 --
 561 -- However, we get can get jolly unhelpful error messages.
 562 --      e.g.    foo = id runST
 563 --
 564 --    Inferred type is less polymorphic than expected
 565 --      Quantified type variable `s' escapes
 566 --      Expected type: ST s a -> t
 567 --      Inferred type: (forall s1. ST s1 a) -> a
 568 --    In the first argument of `id', namely `runST'
 569 --    In a right-hand side of function `foo': id runST
 570 --
 571 -- I'm not quite sure what to do about this!
 572
 573 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
 574   = do  { (act_arg, act_res) <- unify_fun act_ty
 575         ; tcSub_fun exp_arg exp_res act_arg act_res }
 576
 577 tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
 578   = do  { (exp_arg, exp_res) <- unify_fun exp_ty
 579         ; tcSub_fun exp_arg exp_res act_arg act_res }
 580
 581 -----------------------------------
 582 -- Unification case
 583 -- If none of the above match, we revert to the plain unifier
 584 tc_sub exp_sty expected_ty act_sty actual_ty
 585   = uTys True exp_sty expected_ty True act_sty actual_ty        `thenM_`
 586     returnM idCoercion
 587
 588 -----------------------------------
 589 -- A helper to make a function type match
 590 -- The error message isn't very good, but that's a problem with
 591 -- all of this subsumption code
 592 unify_fun ty
 593   = do { (ok, args, res) <- unify_fun_ty True 1 ty
 594         ; if ok then return (head args, res)
 595           else failWithTc (ptext SLIT("Expecting a function type, but found") <+> quotes (ppr ty))}
 596 \end{code}
 597
 598 \begin{code}
 599 tcSub_fun exp_arg exp_res act_arg act_res
 600   = tc_sub act_arg act_arg exp_arg exp_arg      `thenM` \ co_fn_arg ->
 601     tc_sub exp_res exp_res act_res act_res      `thenM` \ co_fn_res ->
 602     newUnique                                   `thenM` \ uniq ->
 603     let
 604         -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
 605         -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
 606         -- co_fn     :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
 607         arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
 608         coercion | isIdCoercion co_fn_arg,
 609                    isIdCoercion co_fn_res = idCoercion
 610                  | otherwise              = mkCoercion co_fn
 611
 612         co_fn e = DictLam [arg_id]
 613                      (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
 614                 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
 615                 --      HsVar arg_id :: HsExpr exp_arg
 616                 --      co_fn_arg $it :: HsExpr act_arg
 617                 --      HsApp e $it   :: HsExpr act_res
 618                 --      co_fn_res $it :: HsExpr exp_res
 619     in
 620     returnM coercion
 621 \end{code}
 622
 623
 624 %************************************************************************
 625 %*                                                                      *
 626 \subsection{Generalisation}
 627 %*                                                                      *
 628 %************************************************************************
 629
 630 \begin{code}
 631 tcGen :: TcSigmaType                            -- expected_ty
 632       -> TcTyVarSet                             -- Extra tyvars that the universally
 633                                                 --      quantified tyvars of expected_ty
 634                                                 --      must not be unified
 635       -> (TcRhoType -> TcM result)              -- spec_ty
 636       -> TcM (ExprCoFn, result)
 637         -- The expression has type: spec_ty -> expected_ty
 638
 639 tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
 640                                                 -- If not, the call is a no-op
 641   = do  {       -- We want the GenSkol info in the skolemised type variables to
 642                 -- mention the *instantiated* tyvar names, so that we get a
 643                 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
 644                 -- Hence the tiresome but innocuous fixM
 645           ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
 646                 do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
 647                    ; span <- getSrcSpanM
 648                    ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
 649                    ; return ((forall_tvs, theta, rho_ty), skol_info) })
 650
 651 #ifdef DEBUG
 652         ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
 653                                     text "expected_ty" <+> ppr expected_ty,
 654                                     text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
 655                                     text "free_tvs" <+> ppr free_tvs,
 656                                     text "forall_tvs" <+> ppr forall_tvs])
 657 #endif
 658
 659         -- Type-check the arg and unify with poly type
 660         ; (result, lie) <- getLIE (thing_inside rho_ty)
 661
 662         -- Check that the "forall_tvs" havn't been constrained
 663         -- The interesting bit here is that we must include the free variables
 664         -- of the expected_ty.  Here's an example:
 665         --       runST (newVar True)
 666         -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
 667         -- for (newVar True), with s fresh.  Then we unify with the runST's arg type
 668         -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
 669         -- So now s' isn't unconstrained because it's linked to a.
 670         -- Conclusion: include the free vars of the expected_ty in the
 671         -- list of "free vars" for the signature check.
 672
 673         ; dicts <- newDicts (SigOrigin skol_info) theta
 674         ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
 675
 676         ; checkSigTyVarsWrt free_tvs forall_tvs
 677         ; traceTc (text "tcGen:done")
 678
 679         ; let
 680             -- This HsLet binds any Insts which came out of the simplification.
 681             -- It's a bit out of place here, but using AbsBind involves inventing
 682             -- a couple of new names which seems worse.
 683                 dict_ids = map instToId dicts
 684                 co_fn e  = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsDictLet inst_binds (noLoc e)))
 685         ; returnM (mkCoercion co_fn, result) }
 686   where
 687     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
 688     sig_msg  = ptext SLIT("expected type of an expression")
 689 \end{code}
 690
 691
 692
 693 %************************************************************************
 694 %*                                                                      *
 695 \subsection[Unify-exported]{Exported unification functions}
 696 %*                                                                      *
 697 %************************************************************************
 698
 699 The exported functions are all defined as versions of some
 700 non-exported generic functions.
 701
 702 Unify two @TauType@s.  Dead straightforward.
 703
 704 \begin{code}
 705 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 706 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
 707   =     -- The unifier should only ever see tau-types
 708         -- (no quantification whatsoever)
 709     ASSERT2( isTauTy ty1, ppr ty1 )
 710     ASSERT2( isTauTy ty2, ppr ty2 )
 711     addErrCtxtM (unifyCtxt "type" ty1 ty2) $
 712     uTys True ty1 ty1 True ty2 ty2
 713
 714 unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
 715 unifyTheta theta1 theta2
 716   = do { checkTc (equalLength theta1 theta2)
 717                  (ptext SLIT("Contexts differ in length"))
 718        ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
 719 \end{code}
 720
 721 @unifyTauTyList@ unifies corresponding elements of two lists of
 722 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
 723 of equal length.  We charge down the list explicitly so that we can
 724 complain if their lengths differ.
 725
 726 \begin{code}
 727 unifyTauTyLists :: Bool ->  -- Allow refinements on tys1
 728                    [TcTauType] ->
 729                    Bool ->  -- Allow refinements on tys2
 730                    [TcTauType] ->  TcM ()
 731 -- Precondition: lists must be same length
 732 -- Having the caller check gives better error messages
 733 -- Actually the caller neve does  need to check; see Note [Tycon app]
 734 unifyTauTyLists r1 []         r2 []             = returnM ()
 735 unifyTauTyLists r1 (ty1:tys1) r2 (ty2:tys2)     = uTys r1 ty1 ty1 r2 ty2 ty2   `thenM_`
 736                                         unifyTauTyLists r1 tys1 r2 tys2
 737 unifyTauTyLists r1 ty1s r2 ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 738 \end{code}
 739
 740 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 741 all together.  It is used, for example, when typechecking explicit
 742 lists, when all the elts should be of the same type.
 743
 744 \begin{code}
 745 unifyTauTyList :: [TcTauType] -> TcM ()
 746 unifyTauTyList []                = returnM ()
 747 unifyTauTyList [ty]              = returnM ()
 748 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenM_`
 749                                    unifyTauTyList tys
 750 \end{code}
 751
 752 %************************************************************************
 753 %*                                                                      *
 754 \subsection[Unify-uTys]{@uTys@: getting down to business}
 755 %*                                                                      *
 756 %************************************************************************
 757
 758 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 759 we want to report errors in terms of synomyms if poss.  The first of
 760 the pair is used in error messages only; it is always the same as the
 761 second, except that if the first is a synonym then the second may be a
 762 de-synonym'd version.  This way we get better error messages.
 763
 764 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 765
 766 \begin{code}
 767 uTys :: Bool                    -- Allow refinements to ty1
 768      -> TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 769                                 -- ty1 is the *expected* type
 770      -> Bool                    -- Allow refinements to ty2
 771      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 772                                 -- ty2 is the *actual* type
 773      -> TcM ()
 774
 775         -- Always expand synonyms (see notes at end)
 776         -- (this also throws away FTVs)
 777 uTys r1 ps_ty1 (NoteTy n1 ty1) r2 ps_ty2 ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
 778 uTys r1 ps_ty1 ty1 r2 ps_ty2 (NoteTy n2 ty2) = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
 779
 780         -- Variables; go for uVar
 781 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
 782 uTys r1 ps_ty1 ty1 r2 ps_ty2 (TyVarTy tyvar2) = uVar True  r2 tyvar2 r1 ps_ty1 ty1
 783                                         -- "True" means args swapped
 784
 785         -- Predicates
 786 uTys r1 _ (PredTy (IParam n1 t1)) r2 _ (PredTy (IParam n2 t2))
 787   | n1 == n2 = uTys r1 t1 t1 r2 t2 t2
 788 uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2))
 789   | c1 == c2 = unifyTauTyLists r1 tys1 r2 tys2
 790         -- Guaranteed equal lengths because the kinds check
 791
 792         -- Functions; just check the two parts
 793 uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2)
 794   = uTys r1 fun1 fun1 r2 fun2 fun2      `thenM_`    uTys r1 arg1 arg1 r2 arg2 arg2
 795
 796         -- Type constructors must match
 797 uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2)
 798   | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2
 799         -- See Note [TyCon app]
 800
 801         -- Applications need a bit of care!
 802         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 803         -- NB: we've already dealt with type variables and Notes,
 804         -- so if one type is an App the other one jolly well better be too
 805 uTys r1 ps_ty1 (AppTy s1 t1) r2 ps_ty2 ty2
 806   = case tcSplitAppTy_maybe ty2 of
 807         Just (s2,t2) -> uTys r1 s1 s1 r2 s2 s2  `thenM_`    uTys r1 t1 t1 r2 t2 t2
 808         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 809
 810         -- Now the same, but the other way round
 811         -- Don't swap the types, because the error messages get worse
 812 uTys r1 ps_ty1 ty1 r2 ps_ty2 (AppTy s2 t2)
 813   = case tcSplitAppTy_maybe ty1 of
 814         Just (s1,t1) -> uTys r1 s1 s1 r2 s2 s2  `thenM_`    uTys r1 t1 t1 r2 t2 t2
 815         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 816
 817         -- Not expecting for-alls in unification
 818         -- ... but the error message from the unifyMisMatch more informative
 819         -- than a panic message!
 820
 821         -- Anything else fails
 822 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 823 \end{code}
 824
 825 Note [Tycon app]
 826 ~~~~~~~~~~~~~~~~
 827 When we find two TyConApps, the argument lists are guaranteed equal
 828 length.  Reason: intially the kinds of the two types to be unified is
 829 the same. The only way it can become not the same is when unifying two
 830 AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
 831 the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
 832 which we do, that ensures that f1,f2 have the same kind; and that
 833 means a1,a2 have the same kind.  And now the argument repeats.
 834
 835
 836 Notes on synonyms
 837 ~~~~~~~~~~~~~~~~~
 838 If you are tempted to make a short cut on synonyms, as in this
 839 pseudocode...
 840
 841 \begin{verbatim}
 842 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 843 -- NO     = if (con1 == con2) then
 844 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
 845 -- NO   -- by unifying their arguments and ignoring their expansions.
 846 -- NO   unifyTauTypeLists args1 args2
 847 -- NO    else
 848 -- NO   -- Never mind.  Just expand them and try again
 849 -- NO   uTys ty1 ty2
 850 \end{verbatim}
 851
 852 then THINK AGAIN.  Here is the whole story, as detected and reported
 853 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 854 \begin{quotation}
 855 Here's a test program that should detect the problem:
 856
 857 \begin{verbatim}
 858         type Bogus a = Int
 859         x = (1 :: Bogus Char) :: Bogus Bool
 860 \end{verbatim}
 861
 862 The problem with [the attempted shortcut code] is that
 863 \begin{verbatim}
 864         con1 == con2
 865 \end{verbatim}
 866 is not a sufficient condition to be able to use the shortcut!
 867 You also need to know that the type synonym actually USES all
 868 its arguments.  For example, consider the following type synonym
 869 which does not use all its arguments.
 870 \begin{verbatim}
 871         type Bogus a = Int
 872 \end{verbatim}
 873
 874 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 875 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 876 would fail, even though the expanded forms (both \tr{Int}) should
 877 match.
 878
 879 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 880 unnecessarily bind \tr{t} to \tr{Char}.
 881
 882 ... You could explicitly test for the problem synonyms and mark them
 883 somehow as needing expansion, perhaps also issuing a warning to the
 884 user.
 885 \end{quotation}
 886
 887
 888 %************************************************************************
 889 %*                                                                      *
 890 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 891 %*                                                                      *
 892 %************************************************************************
 893
 894 @uVar@ is called when at least one of the types being unified is a
 895 variable.  It does {\em not} assume that the variable is a fixed point
 896 of the substitution; rather, notice that @uVar@ (defined below) nips
 897 back into @uTys@ if it turns out that the variable is already bound.
 898
 899 \begin{code}
 900 uVar :: Bool            -- False => tyvar is the "expected"
 901                         -- True  => ty    is the "expected" thing
 902      -> Bool            -- True, allow refinements to tv1, False don't
 903      -> TcTyVar
 904      -> Bool            -- Allow refinements to ty2?
 905      -> TcTauType -> TcTauType  -- printing and real versions
 906      -> TcM ()
 907
 908 uVar swapped r1 tv1 r2 ps_ty2 ty2
 909   = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2))       `thenM_`
 910     condLookupTcTyVar r1 tv1    `thenM` \ details ->
 911     case details of
 912         IndirectTv r1' ty1 | swapped   -> uTys r2   ps_ty2 ty2 r1' ty1    ty1   -- Swap back
 913                            | otherwise -> uTys r1' ty1     ty1 r2  ps_ty2 ty2   -- Same order
 914         DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
 915
 916 ----------------
 917 uDoneVar :: Bool                        -- Args are swapped
 918          -> TcTyVar -> TcTyVarDetails   -- Tyvar 1
 919          -> Bool                        -- Allow refinements to ty2
 920          -> TcTauType -> TcTauType      -- Type 2
 921          -> TcM ()
 922 -- Invariant: tyvar 1 is not unified with anything
 923
 924 uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
 925   =     -- Expand synonyms; ignore FTVs
 926     uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
 927
 928 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
 929         -- Same type variable => no-op
 930   | tv1 == tv2
 931   = returnM ()
 932
 933         -- Distinct type variables
 934   | otherwise
 935   = do  { lookup2 <- condLookupTcTyVar r2 tv2
 936         ; case lookup2 of
 937                 IndirectTv b ty2' -> uDoneVar  swapped tv1 details1 b ty2' ty2'
 938                 DoneTv details2   -> uDoneVars swapped tv1 details1 tv2 details2
 939         }
 940
 941 uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2     -- ty2 is not a type variable
 942   = case details1 of
 943         MetaTv ref1 -> do {     -- Do the occurs check, and check that we are not
 944                                 -- unifying a type variable with a polytype
 945                                 -- Returns a zonked type ready for the update
 946                             ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
 947                           ; updateMeta swapped tv1 ref1 ty2 }
 948
 949         skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
 950
 951
 952 ----------------
 953 uDoneVars :: Bool                       -- Args are swapped
 954           -> TcTyVar -> TcTyVarDetails  -- Tyvar 1
 955           -> TcTyVar -> TcTyVarDetails  -- Tyvar 2
 956           -> TcM ()
 957 -- Invarant: the type variables are distinct,
 958 -- and are not already unified with anything
 959
 960 uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
 961   = case details2 of
 962         MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 963         other                    -> updateMeta swapped       tv1 ref1 (mkTyVarTy tv2)
 964         -- Note that updateMeta does a sub-kind check
 965         -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
 966   where
 967     k1 = tyVarKind tv1
 968     k2 = tyVarKind tv2
 969     update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
 970         -- Update the variable with least kind info
 971         -- See notes on type inference in Kind.lhs
 972         -- The "nicer to" part only applies if the two kinds are the same,
 973         -- so we can choose which to do.
 974
 975     nicer_to_update_tv2 = isSystemName (varName tv2)
 976         -- Try to update sys-y type variables in preference to ones
 977         -- gotten (say) by instantiating a polymorphic function with
 978         -- a user-written type sig
 979
 980 uDoneVars swapped tv1 (SkolemTv _) tv2 details2
 981   = case details2 of
 982         MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 983         other       -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
 984
 985 uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
 986   = case details2 of
 987         MetaTv ref2   -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
 988         SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
 989         other         -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
 990
 991 ----------------
 992 updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 993 -- Update tv1, which is flexi; occurs check is alrady done
 994 updateMeta swapped tv1 ref1 ty2
 995   = do  { checkKinds swapped tv1 ty2
 996         ; writeMutVar ref1 (Indirect ty2) }
 997 \end{code}
 998
 999 \begin{code}
1000 checkKinds swapped tv1 ty2
1001 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1002 -- ty2 has been zonked at this stage, which ensures that
1003 -- its kind has as much boxity information visible as possible.
1004   | tk2 `isSubKind` tk1 = returnM ()
1005
1006   | otherwise
1007         -- Either the kinds aren't compatible
1008         --      (can happen if we unify (a b) with (c d))
1009         -- or we are unifying a lifted type variable with an
1010         --      unlifted type: e.g.  (id 3#) is illegal
1011   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1012     unifyKindMisMatch k1 k2
1013   where
1014     (k1,k2) | swapped   = (tk2,tk1)
1015             | otherwise = (tk1,tk2)
1016     tk1 = tyVarKind tv1
1017     tk2 = typeKind ty2
1018 \end{code}
1019
1020 \begin{code}
1021 checkValue tv1 r2 ps_ty2 non_var_ty2
1022 -- Do the occurs check, and check that we are not
1023 -- unifying a type variable with a polytype
1024 -- Return the type to update the type variable with, or fail
1025
1026 -- Basically we want to update     tv1 := ps_ty2
1027 -- because ps_ty2 has type-synonym info, which improves later error messages
1028 --
1029 -- But consider
1030 --      type A a = ()
1031 --
1032 --      f :: (A a -> a -> ()) -> ()
1033 --      f = \ _ -> ()
1034 --
1035 --      x :: ()
1036 --      x = f (\ x p -> p x)
1037 --
1038 -- In the application (p x), we try to match "t" with "A t".  If we go
1039 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1040 -- an infinite loop later.
1041 -- But we should not reject the program, because A t = ().
1042 -- Rather, we should bind t to () (= non_var_ty2).
1043 --
1044 -- That's why we have this two-state occurs-check
1045   = zonk_tc_type r2 ps_ty2                      `thenM` \ ps_ty2' ->
1046     case okToUnifyWith tv1 ps_ty2' of {
1047         Nothing -> returnM ps_ty2' ;    -- Success
1048         other ->
1049
1050     zonk_tc_type r2 non_var_ty2         `thenM` \ non_var_ty2' ->
1051     case okToUnifyWith tv1 non_var_ty2' of
1052         Nothing ->      -- This branch rarely succeeds, except in strange cases
1053                         -- like that in the example above
1054                     returnM non_var_ty2'
1055
1056         Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
1057     }
1058   where
1059     zonk_tc_type refine ty
1060       = zonkType (\tv -> return (TyVarTy tv)) refine ty
1061         -- We may already be inside a wobbly type t2, and
1062         -- should take that into account here
1063
1064 data Problem = OccurCheck | NotMonoType
1065
1066 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
1067 -- (okToUnifyWith tv ty) checks whether it's ok to unify
1068 --      tv :=: ty
1069 -- Nothing => ok
1070 -- Just p  => not ok, problem p
1071
1072 okToUnifyWith tv ty
1073   = ok ty
1074   where
1075     ok (TyVarTy tv') | tv == tv' = Just OccurCheck
1076                      | otherwise = Nothing
1077     ok (AppTy t1 t2)            = ok t1 `and` ok t2
1078     ok (FunTy t1 t2)            = ok t1 `and` ok t2
1079     ok (TyConApp _ ts)          = oks ts
1080     ok (ForAllTy _ _)           = Just NotMonoType
1081     ok (PredTy st)              = ok_st st
1082     ok (NoteTy (FTVNote _) t)   = ok t
1083     ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
1084                 -- Type variables may be free in t1 but not t2
1085                 -- A forall may be in t2 but not t1
1086
1087     oks ts = foldr (and . ok) Nothing ts
1088
1089     ok_st (ClassP _ ts) = oks ts
1090     ok_st (IParam _ t)  = ok t
1091
1092     Nothing `and` m = m
1093     Just p  `and` m = Just p
1094 \end{code}
1095
1096
1097 %************************************************************************
1098 %*                                                                      *
1099                 Kind unification
1100 %*                                                                      *
1101 %************************************************************************
1102
1103 Unifying kinds is much, much simpler than unifying types.
1104
1105 \begin{code}
1106 unifyKind :: TcKind                 -- Expected
1107           -> TcKind                 -- Actual
1108           -> TcM ()
1109 unifyKind LiftedTypeKind   LiftedTypeKind   = returnM ()
1110 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
1111
1112 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
1113 unifyKind ArgTypeKind  k2 | isArgTypeKind k2    = returnM ()
1114   -- Respect sub-kinding
1115
1116 unifyKind (FunKind a1 r1) (FunKind a2 r2)
1117  = do { unifyKind a2 a1; unifyKind r1 r2 }
1118                 -- Notice the flip in the argument,
1119                 -- so that the sub-kinding works right
1120
1121 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
1122 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
1123 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1124
1125 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1126 unifyKinds []       []       = returnM ()
1127 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenM_`
1128                                unifyKinds ks1 ks2
1129 unifyKinds _ _               = panic "unifyKinds: length mis-match"
1130
1131 ----------------
1132 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1133 uKVar swapped kv1 k2
1134   = do  { mb_k1 <- readKindVar kv1
1135         ; case mb_k1 of
1136             Nothing -> uUnboundKVar swapped kv1 k2
1137             Just k1 | swapped   -> unifyKind k2 k1
1138                     | otherwise -> unifyKind k1 k2 }
1139
1140 ----------------
1141 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1142 uUnboundKVar swapped kv1 k2@(KindVar kv2)
1143   | kv1 == kv2 = returnM ()
1144   | otherwise   -- Distinct kind variables
1145   = do  { mb_k2 <- readKindVar kv2
1146         ; case mb_k2 of
1147             Just k2 -> uUnboundKVar swapped kv1 k2
1148             Nothing -> writeKindVar kv1 k2 }
1149
1150 uUnboundKVar swapped kv1 non_var_k2
1151   = do  { k2' <- zonkTcKind non_var_k2
1152         ; kindOccurCheck kv1 k2'
1153         ; k2'' <- kindSimpleKind swapped k2'
1154                 -- KindVars must be bound only to simple kinds
1155                 -- Polarities: (kindSimpleKind True ?) succeeds
1156                 -- returning *, corresponding to unifying
1157                 --      expected: ?
1158                 --      actual:   kind-ver
1159         ; writeKindVar kv1 k2'' }
1160
1161 ----------------
1162 kindOccurCheck kv1 k2   -- k2 is zonked
1163   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1164   where
1165     not_in (KindVar kv2)   = kv1 /= kv2
1166     not_in (FunKind a2 r2) = not_in a2 && not_in r2
1167     not_in other           = True
1168
1169 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1170 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1171 -- If the flag is False, it requires k <: sk
1172 -- E.g.         kindSimpleKind False ?? = *
1173 -- What about (kv -> *) :=: ?? -> *
1174 kindSimpleKind orig_swapped orig_kind
1175   = go orig_swapped orig_kind
1176   where
1177     go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
1178                                ; k2' <- go sw k2
1179                                ; return (FunKind k1' k2') }
1180     go True OpenTypeKind = return liftedTypeKind
1181     go True ArgTypeKind  = return liftedTypeKind
1182     go sw LiftedTypeKind  = return liftedTypeKind
1183     go sw k@(KindVar _)   = return k    -- KindVars are always simple
1184     go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1185                                   <+> ppr orig_swapped <+> ppr orig_kind)
1186         -- I think this can't actually happen
1187
1188 -- T v = MkT v           v must be a type
1189 -- T v w = MkT (v -> w)  v must not be an umboxed tuple
1190
1191 ----------------
1192 kindOccurCheckErr tyvar ty
1193   = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1194        2 (sep [ppr tyvar, char '=', ppr ty])
1195
1196 unifyKindMisMatch ty1 ty2
1197   = zonkTcKind ty1      `thenM` \ ty1' ->
1198     zonkTcKind ty2      `thenM` \ ty2' ->
1199     let
1200         msg = hang (ptext SLIT("Couldn't match kind"))
1201                    2 (sep [quotes (ppr ty1'),
1202                            ptext SLIT("against"),
1203                            quotes (ppr ty2')])
1204     in
1205     failWithTc msg
1206 \end{code}
1207
1208 \begin{code}
1209 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1210 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1211
1212 unifyFunKind (KindVar kvar)
1213   = readKindVar kvar    `thenM` \ maybe_kind ->
1214     case maybe_kind of
1215         Just fun_kind -> unifyFunKind fun_kind
1216         Nothing       -> do { arg_kind <- newKindVar
1217                             ; res_kind <- newKindVar
1218                             ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1219                             ; returnM (Just (arg_kind,res_kind)) }
1220
1221 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1222 unifyFunKind other                       = returnM Nothing
1223 \end{code}
1224
1225 %************************************************************************
1226 %*                                                                      *
1227 \subsection[Unify-context]{Errors and contexts}
1228 %*                                                                      *
1229 %************************************************************************
1230
1231 Errors
1232 ~~~~~~
1233
1234 \begin{code}
1235 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
1236   = zonkTcType ty1      `thenM` \ ty1' ->
1237     zonkTcType ty2      `thenM` \ ty2' ->
1238     returnM (err ty1' ty2')
1239   where
1240     err ty1 ty2 = (env1,
1241                    nest 2
1242                         (vcat [
1243                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1244                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1245                         ]))
1246                   where
1247                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1248
1249 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
1250         -- tv1 and ty2 are zonked already
1251   = returnM msg
1252   where
1253     msg = (env2, ptext SLIT("When matching the kinds of") <+>
1254                  sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1255
1256     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
1257                              | otherwise = (pp1, pp2)
1258     (env1, tv1') = tidyOpenTyVar tidy_env tv1
1259     (env2, ty2') = tidyOpenType  env1 ty2
1260     pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1261     pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1262
1263 unifyMisMatch ty1 ty2
1264   = do  { (env, msg) <- misMatchMsg ty1 ty2
1265         ; failWithTcM (env, msg) }
1266
1267 misMatchMsg ty1 ty2
1268   = do  { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
1269         ; (env2, pp2, extra2) <- ppr_ty env1 ty2
1270         ; return (env2, sep [sep [ptext SLIT("Couldn't match") <+> pp1,
1271                                   nest 7 (ptext SLIT("against") <+> pp2)],
1272                              nest 2 extra1, nest 2 extra2]) }
1273
1274 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1275 ppr_ty env ty
1276   = do { ty' <- zonkTcType ty
1277        ; let (env1,tidy_ty) = tidyOpenType env ty'
1278              simple_result  = (env1, quotes (ppr tidy_ty), empty)
1279        ; case tidy_ty of
1280            TyVarTy tv
1281                 | isSkolemTyVar tv -> return (env2, pp_rigid tv',
1282                                               pprTcTyVar tv')
1283                 | otherwise -> return simple_result
1284                 where
1285                   (env2, tv') = tidySkolemTyVar env1 tv
1286            other -> return simple_result }
1287   where
1288     pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
1289
1290 unifyCheck problem tyvar ty
1291   = (env2, hang msg
1292               2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1293   where
1294     (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1295     (env2, tidy_ty)    = tidyOpenType  env1         ty
1296
1297     msg = case problem of
1298             OccurCheck  -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1299             NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1300 \end{code}
1301
1302
1303 %************************************************************************
1304 %*                                                                      *
1305         Checking kinds
1306 %*                                                                      *
1307 %************************************************************************
1308
1309 ---------------------------
1310 -- We would like to get a decent error message from
1311 --   (a) Under-applied type constructors
1312 --              f :: (Maybe, Maybe)
1313 --   (b) Over-applied type constructors
1314 --              f :: Int x -> Int x
1315 --
1316
1317 \begin{code}
1318 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1319 -- A fancy wrapper for 'unifyKind', which tries
1320 -- to give decent error messages.
1321 checkExpectedKind ty act_kind exp_kind
1322   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1323   = returnM ()
1324   | otherwise
1325   = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
1326     case mb_r of {
1327         Just r  -> returnM () ; -- Unification succeeded
1328         Nothing ->
1329
1330         -- So there's definitely an error
1331         -- Now to find out what sort
1332     zonkTcKind exp_kind         `thenM` \ exp_kind ->
1333     zonkTcKind act_kind         `thenM` \ act_kind ->
1334
1335     let (exp_as, _) = splitKindFunTys exp_kind
1336         (act_as, _) = splitKindFunTys act_kind
1337         n_exp_as = length exp_as
1338         n_act_as = length act_as
1339
1340         (env1, tidy_exp_kind) = tidyKind emptyTidyEnv exp_kind
1341         (env2, tidy_act_kind) = tidyKind env1         act_kind
1342
1343         err | n_exp_as < n_act_as       -- E.g. [Maybe]
1344             = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1345
1346                 -- Now n_exp_as >= n_act_as. In the next two cases,
1347                 -- n_exp_as == 0, and hence so is n_act_as
1348             | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1349             = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1350                 <+> ptext SLIT("is unlifted")
1351
1352             | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1353             = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1354                 <+> ptext SLIT("is lifted")
1355
1356             | otherwise                 -- E.g. Monad [Int]
1357             = ptext SLIT("Kind mis-match")
1358
1359         more_info = sep [ ptext SLIT("Expected kind") <+>
1360                                 quotes (pprKind tidy_exp_kind) <> comma,
1361                           ptext SLIT("but") <+> quotes (ppr ty) <+>
1362                                 ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
1363    in
1364    failWithTcM (env2, err $$ more_info)
1365    }
1366 \end{code}
1367
1368 %************************************************************************
1369 %*                                                                      *
1370 \subsection{Checking signature type variables}
1371 %*                                                                      *
1372 %************************************************************************
1373
1374 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1375 are not mentioned in the environment.  In particular:
1376
1377         (a) Not mentioned in the type of a variable in the envt
1378                 eg the signature for f in this:
1379
1380                         g x = ... where
1381                                         f :: a->[a]
1382                                         f y = [x,y]
1383
1384                 Here, f is forced to be monorphic by the free occurence of x.
1385
1386         (d) Not (unified with another type variable that is) in scope.
1387                 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1388             when checking the expression type signature, we find that
1389             even though there is nothing in scope whose type mentions r,
1390             nevertheless the type signature for the expression isn't right.
1391
1392             Another example is in a class or instance declaration:
1393                 class C a where
1394                    op :: forall b. a -> b
1395                    op x = x
1396             Here, b gets unified with a
1397
1398 Before doing this, the substitution is applied to the signature type variable.
1399
1400 \begin{code}
1401 checkSigTyVars :: [TcTyVar] -> TcM ()
1402 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1403
1404 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1405 checkSigTyVarsWrt extra_tvs sig_tvs
1406   = zonkTcTyVarsAndFV (varSetElems extra_tvs)   `thenM` \ extra_tvs' ->
1407     check_sig_tyvars extra_tvs' sig_tvs
1408
1409 check_sig_tyvars
1410         :: TcTyVarSet   -- Global type variables. The universally quantified
1411                         --      tyvars should not mention any of these
1412                         --      Guaranteed already zonked.
1413         -> [TcTyVar]    -- Universally-quantified type variables in the signature
1414                         --      Guaranteed to be skolems
1415         -> TcM ()
1416 check_sig_tyvars extra_tvs []
1417   = returnM ()
1418 check_sig_tyvars extra_tvs sig_tvs
1419   = ASSERT( all isSkolemTyVar sig_tvs )
1420     do  { gbl_tvs <- tcGetGlobalTyVars
1421         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1422                                       text "gbl_tvs" <+> ppr gbl_tvs,
1423                                       text "extra_tvs" <+> ppr extra_tvs]))
1424
1425         ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1426         ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
1427               (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1428         }
1429
1430 bleatEscapedTvs :: TcTyVarSet   -- The global tvs
1431                 -> [TcTyVar]    -- The possibly-escaping type variables
1432                 -> [TcTyVar]    -- The zonked versions thereof
1433                 -> TcM ()
1434 -- Complain about escaping type variables
1435 -- We pass a list of type variables, at least one of which
1436 -- escapes.  The first list contains the original signature type variable,
1437 -- while the second  contains the type variable it is unified to (usually itself)
1438 bleatEscapedTvs globals sig_tvs zonked_tvs
1439   = do  { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1440         ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1441   where
1442     (env1, tidy_tvs)         = tidyOpenTyVars emptyTidyEnv sig_tvs
1443     (env2, tidy_zonked_tvs) = tidyOpenTyVars env1         zonked_tvs
1444
1445     main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1446
1447     check (tidy_env, msgs) (sig_tv, zonked_tv)
1448       | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1449       | otherwise
1450       = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
1451            ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1452
1453 -----------------------
1454 escape_msg sig_tv zonked_tv globs
1455   | notNull globs
1456   = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
1457           nest 2 (vcat globs)]
1458   | otherwise
1459   = msg <+> ptext SLIT("escapes")
1460         -- Sigh.  It's really hard to give a good error message
1461         -- all the time.   One bad case is an existential pattern match.
1462         -- We rely on the "When..." context to help.
1463   where
1464     msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1465     is_bound_to
1466         | sig_tv == zonked_tv = empty
1467         | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
1468 \end{code}
1469
1470 These two context are used with checkSigTyVars
1471
1472 \begin{code}
1473 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1474         -> TidyEnv -> TcM (TidyEnv, Message)
1475 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1476   = zonkTcType sig_tau          `thenM` \ actual_tau ->
1477     let
1478         (env1, tidy_sig_tvs)    = tidyOpenTyVars tidy_env sig_tvs
1479         (env2, tidy_sig_rho)    = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1480         (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1481         sub_msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1482                         ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1483                    ]
1484         msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
1485                     nest 2 sub_msg]
1486     in
1487     returnM (env3, msg)
1488 \end{code}