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