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