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