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