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