compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 Monadic type operations
   7
   8 This module contains monadic operations over types that contain
   9 mutable type variables
  10
  11 \begin{code}
  12 {-# OPTIONS -w #-}
  13 -- The above warning supression flag is a temporary kludge.
  14 -- While working on this module you are encouraged to remove it and fix
  15 -- any warnings in the module. See
  16 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  17 -- for details
  18
  19 module TcMType (
  20   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
  21
  22   --------------------------------
  23   -- Creating new mutable type variables
  24   newFlexiTyVar,
  25   newFlexiTyVarTy,              -- Kind -> TcM TcType
  26   newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
  27   newKindVar, newKindVars,
  28   lookupTcTyVar, LookupTyVarResult(..),
  29
  30   newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar,
  31
  32   --------------------------------
  33   -- Boxy type variables
  34   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
  35
  36   --------------------------------
  37   -- Creating new coercion variables
  38   newCoVars, newMetaCoVar,
  39
  40   --------------------------------
  41   -- Instantiation
  42   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
  43   tcInstSigTyVars,
  44   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
  45   tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
  46
  47   --------------------------------
  48   -- Checking type validity
  49   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
  50   SourceTyCtxt(..), checkValidTheta, checkFreeness,
  51   checkValidInstHead, checkValidInstance,
  52   checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
  53   checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
  54   unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
  55
  56   --------------------------------
  57   -- Zonking
  58   zonkType, zonkTcPredType,
  59   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
  60   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
  61   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  62   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
  63
  64   readKindVar, writeKindVar
  65   ) where
  66
  67 #include "HsVersions.h"
  68
  69 -- friends:
  70 import TypeRep
  71 import TcType
  72 import Type
  73 import Coercion
  74 import Class
  75 import TyCon
  76 import Var
  77
  78 -- others:
  79 import TcRnMonad          -- TcType, amongst others
  80 import FunDeps
  81 import Name
  82 import VarSet
  83 import ErrUtils
  84 import DynFlags
  85 import Util
  86 import Maybes
  87 import ListSetOps
  88 import UniqSupply
  89 import SrcLoc
  90 import Outputable
  91
  92 import Control.Monad    ( when, unless )
  93 import Data.List        ( (\\) )
  94 \end{code}
  95
  96
  97 %************************************************************************
  98 %*                                                                      *
  99         Instantiation in general
 100 %*                                                                      *
 101 %************************************************************************
 102
 103 \begin{code}
 104 tcInstType :: ([TyVar] -> TcM [TcTyVar])                -- How to instantiate the type variables
 105            -> TcType                                    -- Type to instantiate
 106            -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
 107                 -- (type vars (excl coercion vars), preds (incl equalities), rho)
 108 tcInstType inst_tyvars ty
 109   = case tcSplitForAllTys ty of
 110         ([],     rho) -> let    -- There may be overloading despite no type variables;
 111                                 --      (?x :: Int) => Int -> Int
 112                            (theta, tau) = tcSplitPhiTy rho
 113                          in
 114                          return ([], theta, tau)
 115
 116         (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 117
 118                             ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
 119                                 -- Either the tyvars are freshly made, by inst_tyvars,
 120                                 -- or (in the call from tcSkolSigType) any nested foralls
 121                                 -- have different binders.  Either way, zipTopTvSubst is ok
 122
 123                             ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
 124                             ; return (tyvars', theta, tau) }
 125 \end{code}
 126
 127
 128 %************************************************************************
 129 %*                                                                      *
 130         Updating tau types
 131 %*                                                                      *
 132 %************************************************************************
 133
 134 Can't be in TcUnify, as we also need it in TcTyFuns.
 135
 136 \begin{code}
 137 type SwapFlag = Bool
 138         -- False <=> the two args are (actual, expected) respectively
 139         -- True  <=> the two args are (expected, actual) respectively
 140
 141 checkUpdateMeta :: SwapFlag
 142                 -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 143 -- Update tv1, which is flexi; occurs check is alrady done
 144 -- The 'check' version does a kind check too
 145 -- We do a sub-kind check here: we might unify (a b) with (c d)
 146 --      where b::*->* and d::*; this should fail
 147
 148 checkUpdateMeta swapped tv1 ref1 ty2
 149   = do  { checkKinds swapped tv1 ty2
 150         ; updateMeta tv1 ref1 ty2 }
 151
 152 updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
 153 updateMeta tv1 ref1 ty2
 154   = ASSERT( isMetaTyVar tv1 )
 155     ASSERT( isBoxyTyVar tv1 || isTauTy ty2 )
 156     do  { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 )
 157         ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2)
 158         ; writeMutVar ref1 (Indirect ty2)
 159         }
 160
 161 ----------------
 162 checkKinds swapped tv1 ty2
 163 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 164 -- ty2 has been zonked at this stage, which ensures that
 165 -- its kind has as much boxity information visible as possible.
 166   | tk2 `isSubKind` tk1 = return ()
 167
 168   | otherwise
 169         -- Either the kinds aren't compatible
 170         --      (can happen if we unify (a b) with (c d))
 171         -- or we are unifying a lifted type variable with an
 172         --      unlifted type: e.g.  (id 3#) is illegal
 173   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
 174     unifyKindMisMatch k1 k2
 175   where
 176     (k1,k2) | swapped   = (tk2,tk1)
 177             | otherwise = (tk1,tk2)
 178     tk1 = tyVarKind tv1
 179     tk2 = typeKind ty2
 180
 181 ----------------
 182 checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 183 --    (checkTauTvUpdate tv ty)
 184 -- We are about to update the TauTv tv with ty.
 185 -- Check (a) that tv doesn't occur in ty (occurs check)
 186 --       (b) that ty is a monotype
 187 -- Furthermore, in the interest of (b), if you find an
 188 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
 189 --
 190 -- We have three possible outcomes:
 191 -- (1) Return the (non-boxy) type to update the type variable with,
 192 --     [we know the update is ok!]
 193 -- (2) return Nothing, or
 194 --     [we cannot tell whether the update is ok right now]
 195 -- (3) fails.
 196 --     [the update is definitely invalid]
 197 -- We return Nothing in case the tv occurs in ty *under* a type family
 198 -- application.  In this case, we must not update tv (to avoid a cyclic type
 199 -- term), but we also cannot fail claiming an infinite type.  Given
 200 --   type family F a
 201 --   type instance F Int = Int
 202 -- consider
 203 --   a ~ F a
 204 -- This is perfectly reasonable, if we later get a ~ Int.
 205
 206 checkTauTvUpdate orig_tv orig_ty
 207   = do { result <- go orig_ty
 208        ; case result of
 209            Right ty    -> return $ Just ty
 210            Left  True  -> return $ Nothing
 211            Left  False -> occurCheckErr (mkTyVarTy orig_tv) orig_ty
 212        }
 213   where
 214     go :: TcType -> TcM (Either Bool TcType)
 215     -- go returns
 216     --   Right ty    if everything is fine
 217     --   Left True   if orig_tv occurs in orig_ty, but under a type family app
 218     --   Left False  if orig_tv occurs in orig_ty (with no type family app)
 219     -- It fails if it encounters a forall type, except as an argument for a
 220     -- closed type synonym that expands to a tau type.
 221     go (TyConApp tc tys)
 222         | isSynTyCon tc  = go_syn tc tys
 223         | otherwise      = do { tys' <- mapM go tys
 224                               ; return $ occurs (TyConApp tc) tys' }
 225     go (PredTy p)        = do { p' <- go_pred p
 226                               ; return $ occurs1 PredTy p' }
 227     go (FunTy arg res)   = do { arg' <- go arg
 228                               ; res' <- go res
 229                               ; return $ occurs2 FunTy arg' res' }
 230     go (AppTy fun arg)   = do { fun' <- go fun
 231                               ; arg' <- go arg
 232                               ; return $ occurs2 mkAppTy fun' arg' }
 233                 -- NB the mkAppTy; we might have instantiated a
 234                 -- type variable to a type constructor, so we need
 235                 -- to pull the TyConApp to the top.
 236     go (ForAllTy tv ty) = notMonoType orig_ty           -- (b)
 237
 238     go (TyVarTy tv)
 239         | orig_tv == tv = return $ Left False           -- (a)
 240         | isTcTyVar tv  = go_tyvar tv (tcTyVarDetails tv)
 241         | otherwise     = return $ Right (TyVarTy tv)
 242                  -- Ordinary (non Tc) tyvars
 243                  -- occur inside quantified types
 244
 245     go_pred (ClassP c tys) = do { tys' <- mapM go tys
 246                                 ; return $ occurs (ClassP c) tys' }
 247     go_pred (IParam n ty)  = do { ty' <- go ty
 248                                 ; return $ occurs1 (IParam n) ty' }
 249     go_pred (EqPred t1 t2) = do { t1' <- go t1
 250                                 ; t2' <- go t2
 251                                 ; return $ occurs2 EqPred t1' t2' }
 252
 253     go_tyvar tv (SkolemTv _) = return $ Right (TyVarTy tv)
 254     go_tyvar tv (MetaTv box ref)
 255         = do { cts <- readMutVar ref
 256              ; case cts of
 257                   Indirect ty -> go ty
 258                   Flexi -> case box of
 259                                 BoxTv -> do { ty <- fillBoxWithTau tv ref
 260                                             ; return $ Right ty }
 261                                 other -> return $ Right (TyVarTy tv)
 262              }
 263
 264         -- go_syn is called for synonyms only
 265         -- See Note [Type synonyms and the occur check]
 266     go_syn tc tys
 267         | not (isTauTyCon tc)
 268         = notMonoType orig_ty   -- (b) again
 269         | otherwise
 270         = do { (msgs, mb_tys') <- tryTc (mapM go tys)
 271              ; case mb_tys' of
 272
 273                 -- we had a type error => forall in type parameters
 274                 Nothing
 275                   | isOpenTyCon tc -> notMonoArgs (TyConApp tc tys)
 276                         -- Synonym families must have monotype args
 277                   | otherwise      -> go (expectJust "checkTauTvUpdate(1)"
 278                                             (tcView (TyConApp tc tys)))
 279                         -- Try again, expanding the synonym
 280
 281                 -- no type error, but need to test whether occurs check happend
 282                 Just tys' ->
 283                   case occurs id tys' of
 284                     Left _
 285                       | isOpenTyCon tc -> return $ Left True
 286                         -- Variable occured under type family application
 287                       | otherwise      -> go (expectJust "checkTauTvUpdate(2)"
 288                                                (tcView (TyConApp tc tys)))
 289                         -- Try again, expanding the synonym
 290                     Right raw_tys'     -> return $ Right (TyConApp tc raw_tys')
 291                         -- Retain the synonym (the common case)
 292              }
 293
 294     -- Left results (= occurrence of orig_ty) dominate and
 295     -- (Left False) (= fatal occurrence) dominates over (Left True)
 296     occurs :: ([a] -> b) -> [Either Bool a] -> Either Bool b
 297     occurs c = either Left (Right . c) . foldr combine (Right [])
 298       where
 299         combine (Left famInst1) (Left famInst2) = Left (famInst1 && famInst2)
 300         combine (Right _      ) (Left famInst)  = Left famInst
 301         combine (Left famInst)  (Right _)       = Left famInst
 302         combine (Right arg)     (Right args)    = Right (arg:args)
 303
 304     occurs1 c x   = occurs (\[x']     -> c x')    [x]
 305     occurs2 c x y = occurs (\[x', y'] -> c x' y') [x, y]
 306
 307 fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType
 308 -- (fillBoxWithTau tv ref) fills ref with a freshly allocated
 309 --  tau-type meta-variable, whose print-name is the same as tv
 310 -- Choosing the same name is good: when we instantiate a function
 311 -- we allocate boxy tyvars with the same print-name as the quantified
 312 -- tyvar; and then we often fill the box with a tau-tyvar, and again
 313 -- we want to choose the same name.
 314 fillBoxWithTau tv ref
 315   = do  { tv' <- tcInstTyVar tv         -- Do not gratuitously forget
 316         ; let tau = mkTyVarTy tv'       -- name of the type variable
 317         ; writeMutVar ref (Indirect tau)
 318         ; return tau }
 319 \end{code}
 320
 321 Note [Type synonyms and the occur check]
 322 ~~~~~~~~~~~~~~~~~~~~
 323 Basically we want to update     tv1 := ps_ty2
 324 because ps_ty2 has type-synonym info, which improves later error messages
 325
 326 But consider
 327         type A a = ()
 328
 329         f :: (A a -> a -> ()) -> ()
 330         f = \ _ -> ()
 331
 332         x :: ()
 333         x = f (\ x p -> p x)
 334
 335 In the application (p x), we try to match "t" with "A t".  If we go
 336 ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
 337 an infinite loop later.
 338 But we should not reject the program, because A t = ().
 339 Rather, we should bind t to () (= non_var_ty2).
 340
 341 --------------
 342
 343 Error mesages in case of kind mismatch.
 344
 345 \begin{code}
 346 unifyKindMisMatch ty1 ty2 = do
 347     ty1' <- zonkTcKind ty1
 348     ty2' <- zonkTcKind ty2
 349     let
 350         msg = hang (ptext SLIT("Couldn't match kind"))
 351                    2 (sep [quotes (ppr ty1'),
 352                            ptext SLIT("against"),
 353                            quotes (ppr ty2')])
 354     failWithTc msg
 355
 356 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 357         -- tv1 and ty2 are zonked already
 358   = return msg
 359   where
 360     msg = (env2, ptext SLIT("When matching the kinds of") <+>
 361                  sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
 362
 363     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 364                              | otherwise = (pp1, pp2)
 365     (env1, tv1') = tidyOpenTyVar tidy_env tv1
 366     (env2, ty2') = tidyOpenType  env1 ty2
 367     pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
 368     pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
 369 \end{code}
 370
 371 Error message for failure due to an occurs check.
 372
 373 \begin{code}
 374 occurCheckErr :: TcType -> TcType -> TcM a
 375 occurCheckErr ty containingTy
 376   = do  { env0 <- tcInitTidyEnv
 377         ; ty'           <- zonkTcType ty
 378         ; containingTy' <- zonkTcType containingTy
 379         ; let (env1, tidy_ty1) = tidyOpenType env0 ty'
 380               (env2, tidy_ty2) = tidyOpenType env1 containingTy'
 381               extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
 382         ; failWithTcM (env2, hang msg 2 extra) }
 383   where
 384     msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
 385 \end{code}
 386
 387 %************************************************************************
 388 %*                                                                      *
 389         Kind variables
 390 %*                                                                      *
 391 %************************************************************************
 392
 393 \begin{code}
 394 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
 395 newCoVars spec
 396   = do  { us <- newUniqueSupply
 397         ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
 398                            (mkCoKind ty1 ty2)
 399                  | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
 400
 401 newMetaCoVar :: TcType -> TcType -> TcM TcTyVar
 402 newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2)
 403
 404 newKindVar :: TcM TcKind
 405 newKindVar = do { uniq <- newUnique
 406                 ; ref <- newMutVar Flexi
 407                 ; return (mkTyVarTy (mkKindVar uniq ref)) }
 408
 409 newKindVars :: Int -> TcM [TcKind]
 410 newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
 411 \end{code}
 412
 413
 414 %************************************************************************
 415 %*                                                                      *
 416         SkolemTvs (immutable)
 417 %*                                                                      *
 418 %************************************************************************
 419
 420 \begin{code}
 421 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 422 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 423
 424 tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
 425 -- Instantiate a type signature with skolem constants, but
 426 -- do *not* give them fresh names, because we want the name to
 427 -- be in the type environment -- it is lexically scoped.
 428 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 429
 430 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 431 -- Make skolem constants, but do *not* give them new names, as above
 432 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
 433                               | tv <- tyvars ]
 434
 435 tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
 436 -- Instantiate the tyvar, using
 437 --      * the occ-name and kind of the supplied tyvar,
 438 --      * the unique from the monad,
 439 --      * the location either from the tyvar (mb_loc = Nothing)
 440 --        or from mb_loc (Just loc)
 441 tcInstSkolTyVar info mb_loc tyvar
 442   = do  { uniq <- newUnique
 443         ; let old_name = tyVarName tyvar
 444               kind     = tyVarKind tyvar
 445               loc      = mb_loc `orElse` getSrcSpan old_name
 446               new_name = mkInternalName uniq (nameOccName old_name) loc
 447         ; return (mkSkolTyVar new_name kind info) }
 448
 449 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 450 -- Get the location from the monad
 451 tcInstSkolTyVars info tyvars
 452   = do  { span <- getSrcSpanM
 453         ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
 454
 455 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 456 -- Instantiate a type with fresh skolem constants
 457 -- Binding location comes from the monad
 458 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 459 \end{code}
 460
 461
 462 %************************************************************************
 463 %*                                                                      *
 464         MetaTvs (meta type variables; mutable)
 465 %*                                                                      *
 466 %************************************************************************
 467
 468 \begin{code}
 469 newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
 470 -- Make a new meta tyvar out of thin air
 471 newMetaTyVar box_info kind
 472   = do  { uniq <- newUnique
 473         ; ref <- newMutVar Flexi
 474         ; let name = mkSysTvName uniq fs
 475               fs = case box_info of
 476                         BoxTv   -> FSLIT("t")
 477                         TauTv   -> FSLIT("t")
 478                         SigTv _ -> FSLIT("a")
 479                 -- We give BoxTv and TauTv the same string, because
 480                 -- otherwise we get user-visible differences in error
 481                 -- messages, which are confusing.  If you want to see
 482                 -- the box_info of each tyvar, use -dppr-debug
 483         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 484
 485 instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
 486 -- Make a new meta tyvar whose Name and Kind
 487 -- come from an existing TyVar
 488 instMetaTyVar box_info tyvar
 489   = do  { uniq <- newUnique
 490         ; ref <- newMutVar Flexi
 491         ; let name = setNameUnique (tyVarName tyvar) uniq
 492               kind = tyVarKind tyvar
 493         ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
 494
 495 readMetaTyVar :: TyVar -> TcM MetaDetails
 496 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 497                       readMutVar (metaTvRef tyvar)
 498
 499 isFilledMetaTyVar :: TyVar -> TcM Bool
 500 -- True of a filled-in (Indirect) meta type variable
 501 isFilledMetaTyVar tv
 502   | not (isTcTyVar tv) = return False
 503   | MetaTv _ ref <- tcTyVarDetails tv
 504   = do  { details <- readMutVar ref
 505         ; return (isIndirect details) }
 506   | otherwise = return False
 507
 508 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 509 writeMetaTyVar tyvar ty
 510   | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty)
 511 writeMetaTyVar tyvar ty
 512   | not (isMetaTyVar tyvar)
 513   = pprTrace "writeMetaTyVar" (ppr tyvar) $
 514     return ()
 515   | otherwise
 516   = ASSERT( isMetaTyVar tyvar )
 517     -- TOM: It should also work for coercions
 518     -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
 519     do  { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
 520         ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
 521   where
 522     k1 = tyVarKind tyvar
 523     k2 = typeKind ty
 524 \end{code}
 525
 526
 527 %************************************************************************
 528 %*                                                                      *
 529         MetaTvs: TauTvs
 530 %*                                                                      *
 531 %************************************************************************
 532
 533 \begin{code}
 534 newFlexiTyVar :: Kind -> TcM TcTyVar
 535 newFlexiTyVar kind = newMetaTyVar TauTv kind
 536
 537 newFlexiTyVarTy  :: Kind -> TcM TcType
 538 newFlexiTyVarTy kind = do
 539     tc_tyvar <- newFlexiTyVar kind
 540     return (TyVarTy tc_tyvar)
 541
 542 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 543 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 544
 545 tcInstTyVar :: TyVar -> TcM TcTyVar
 546 -- Instantiate with a META type variable
 547 tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
 548
 549 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 550 -- Instantiate with META type variables
 551 tcInstTyVars tyvars
 552   = do  { tc_tvs <- mapM tcInstTyVar tyvars
 553         ; let tys = mkTyVarTys tc_tvs
 554         ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
 555                 -- Since the tyvars are freshly made,
 556                 -- they cannot possibly be captured by
 557                 -- any existing for-alls.  Hence zipTopTvSubst
 558 \end{code}
 559
 560
 561 %************************************************************************
 562 %*                                                                      *
 563         MetaTvs: SigTvs
 564 %*                                                                      *
 565 %************************************************************************
 566
 567 \begin{code}
 568 tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 569 -- Instantiate with skolems or meta SigTvs; depending on use_skols
 570 -- Always take location info from the supplied tyvars
 571 tcInstSigTyVars use_skols skol_info tyvars
 572   | use_skols
 573   = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
 574
 575   | otherwise
 576   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 577
 578 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 579 zonkSigTyVar sig_tv
 580   | isSkolemTyVar sig_tv
 581   = return sig_tv       -- Happens in the call in TcBinds.checkDistinctTyVars
 582   | otherwise
 583   = ASSERT( isSigTyVar sig_tv )
 584     do { ty <- zonkTcTyVar sig_tv
 585        ; return (tcGetTyVar "zonkSigTyVar" ty) }
 586         -- 'ty' is bound to be a type variable, because SigTvs
 587         -- can only be unified with type variables
 588 \end{code}
 589
 590
 591 %************************************************************************
 592 %*                                                                      *
 593         MetaTvs: BoxTvs
 594 %*                                                                      *
 595 %************************************************************************
 596
 597 \begin{code}
 598 newBoxyTyVar :: Kind -> TcM BoxyTyVar
 599 newBoxyTyVar kind = newMetaTyVar BoxTv kind
 600
 601 newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
 602 newBoxyTyVars kinds = mapM newBoxyTyVar kinds
 603
 604 newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
 605 newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
 606
 607 readFilledBox :: BoxyTyVar -> TcM TcType
 608 -- Read the contents of the box, which should be filled in by now
 609 readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
 610                        do { cts <- readMetaTyVar box_tv
 611                           ; case cts of
 612                                 Flexi -> pprPanic "readFilledBox" (ppr box_tv)
 613                                 Indirect ty -> return ty }
 614
 615 tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
 616 -- Instantiate with a BOXY type variable
 617 tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
 618 \end{code}
 619
 620
 621 %************************************************************************
 622 %*                                                                      *
 623 \subsection{Putting and getting  mutable type variables}
 624 %*                                                                      *
 625 %************************************************************************
 626
 627 But it's more fun to short out indirections on the way: If this
 628 version returns a TyVar, then that TyVar is unbound.  If it returns
 629 any other type, then there might be bound TyVars embedded inside it.
 630
 631 We return Nothing iff the original box was unbound.
 632
 633 \begin{code}
 634 data LookupTyVarResult  -- The result of a lookupTcTyVar call
 635   = DoneTv TcTyVarDetails       -- SkolemTv or virgin MetaTv
 636   | IndirectTv TcType
 637
 638 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 639 lookupTcTyVar tyvar
 640   = ASSERT2( isTcTyVar tyvar, ppr tyvar )
 641     case details of
 642       SkolemTv _   -> return (DoneTv details)
 643       MetaTv _ ref -> do { meta_details <- readMutVar ref
 644                          ; case meta_details of
 645                             Indirect ty -> return (IndirectTv ty)
 646                             Flexi -> return (DoneTv details) }
 647   where
 648     details =  tcTyVarDetails tyvar
 649
 650 {-
 651 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 652 getTcTyVar tyvar
 653   | not (isTcTyVar tyvar)
 654   = pprTrace "getTcTyVar" (ppr tyvar) $
 655     return (Just (mkTyVarTy tyvar))
 656
 657   | otherwise
 658   = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do
 659     maybe_ty <- readMetaTyVar tyvar
 660     case maybe_ty of
 661         Just ty -> do ty' <- short_out ty
 662                       writeMetaTyVar tyvar (Just ty')
 663                       return (Just ty')
 664
 665         Nothing    -> return Nothing
 666
 667 short_out :: TcType -> TcM TcType
 668 short_out ty@(TyVarTy tyvar)
 669   | not (isTcTyVar tyvar)
 670   = return ty
 671
 672   | otherwise = do
 673     maybe_ty <- readMetaTyVar tyvar
 674     case maybe_ty of
 675         Just ty' -> do ty' <- short_out ty'
 676                        writeMetaTyVar tyvar (Just ty')
 677                        return ty'
 678
 679         other    -> return ty
 680
 681 short_out other_ty = return other_ty
 682 -}
 683 \end{code}
 684
 685
 686 %************************************************************************
 687 %*                                                                      *
 688 \subsection{Zonking -- the exernal interfaces}
 689 %*                                                                      *
 690 %************************************************************************
 691
 692 -----------------  Type variables
 693
 694 \begin{code}
 695 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 696 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 697
 698 zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
 699 zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars
 700
 701 zonkTcTyVar :: TcTyVar -> TcM TcType
 702 zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
 703                     zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar
 704 \end{code}
 705
 706 -----------------  Types
 707
 708 \begin{code}
 709 zonkTcType :: TcType -> TcM TcType
 710 zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty
 711
 712 zonkTcTypes :: [TcType] -> TcM [TcType]
 713 zonkTcTypes tys = mapM zonkTcType tys
 714
 715 zonkTcClassConstraints cts = mapM zonk cts
 716     where zonk (clas, tys) = do
 717               new_tys <- zonkTcTypes tys
 718               return (clas, new_tys)
 719
 720 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 721 zonkTcThetaType theta = mapM zonkTcPredType theta
 722
 723 zonkTcPredType :: TcPredType -> TcM TcPredType
 724 zonkTcPredType (ClassP c ts)  = ClassP c <$> zonkTcTypes ts
 725 zonkTcPredType (IParam n t)   = IParam n <$> zonkTcType t
 726 zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
 727 \end{code}
 728
 729 -------------------  These ...ToType, ...ToKind versions
 730                      are used at the end of type checking
 731
 732 \begin{code}
 733 zonkTopTyVar :: TcTyVar -> TcM TcTyVar
 734 -- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
 735 -- to default the kind of ? and ?? etc to *.  This is important to ensure that
 736 -- instance declarations match.  For example consider
 737 --      instance Show (a->b)
 738 --      foo x = show (\_ -> True)
 739 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
 740 -- and that won't match the typeKind (*) in the instance decl.
 741 --
 742 -- Because we are at top level, no further constraints are going to affect these
 743 -- type variables, so it's time to do it by hand.  However we aren't ready
 744 -- to default them fully to () or whatever, because the type-class defaulting
 745 -- rules have yet to run.
 746
 747 zonkTopTyVar tv
 748   | k `eqKind` default_k = return tv
 749   | otherwise
 750   = do  { tv' <- newFlexiTyVar default_k
 751         ; writeMetaTyVar tv (mkTyVarTy tv')
 752         ; return tv' }
 753   where
 754     k = tyVarKind tv
 755     default_k = defaultKind k
 756
 757 zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 758 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
 759
 760 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 761 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 762 --
 763 -- The quantified type variables often include meta type variables
 764 -- we want to freeze them into ordinary type variables, and
 765 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 766 --                      -- see notes with Kind.defaultKind
 767 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
 768 -- bound occurences of the original type variable will get zonked to
 769 -- the immutable version.
 770 --
 771 -- We leave skolem TyVars alone; they are immutable.
 772 zonkQuantifiedTyVar tv
 773   | ASSERT( isTcTyVar tv )
 774     isSkolemTyVar tv = return tv
 775         -- It might be a skolem type variable,
 776         -- for example from a user type signature
 777
 778   | otherwise   -- It's a meta-type-variable
 779   = do  { details <- readMetaTyVar tv
 780
 781         -- Create the new, frozen, skolem type variable
 782         -- We zonk to a skolem, not to a regular TcVar
 783         -- See Note [Zonking to Skolem]
 784         ; let final_kind = defaultKind (tyVarKind tv)
 785               final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
 786
 787         -- Bind the meta tyvar to the new tyvar
 788         ; case details of
 789             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
 790                            return ()
 791                 -- [Sept 04] I don't think this should happen
 792                 -- See note [Silly Type Synonym]
 793
 794             Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 795
 796         -- Return the new tyvar
 797         ; return final_tv }
 798 \end{code}
 799
 800 Note [Silly Type Synonyms]
 801 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 802 Consider this:
 803         type C u a = u  -- Note 'a' unused
 804
 805         foo :: (forall a. C u a -> C u a) -> u
 806         foo x = ...
 807
 808         bar :: Num u => u
 809         bar = foo (\t -> t + t)
 810
 811 * From the (\t -> t+t) we get type  {Num d} =>  d -> d
 812   where d is fresh.
 813
 814 * Now unify with type of foo's arg, and we get:
 815         {Num (C d a)} =>  C d a -> C d a
 816   where a is fresh.
 817
 818 * Now abstract over the 'a', but float out the Num (C d a) constraint
 819   because it does not 'really' mention a.  (see exactTyVarsOfType)
 820   The arg to foo becomes
 821         /\a -> \t -> t+t
 822
 823 * So we get a dict binding for Num (C d a), which is zonked to give
 824         a = ()
 825   [Note Sept 04: now that we are zonking quantified type variables
 826   on construction, the 'a' will be frozen as a regular tyvar on
 827   quantification, so the floated dict will still have type (C d a).
 828   Which renders this whole note moot; happily!]
 829
 830 * Then the /\a abstraction has a zonked 'a' in it.
 831
 832 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 833 a /\a in the final result but all the occurrences of a will be zonked to ()
 834
 835 Note [Zonking to Skolem]
 836 ~~~~~~~~~~~~~~~~~~~~~~~~
 837 We used to zonk quantified type variables to regular TyVars.  However, this
 838 leads to problems.  Consider this program from the regression test suite:
 839
 840   eval :: Int -> String -> String -> String
 841   eval 0 root actual = evalRHS 0 root actual
 842
 843   evalRHS :: Int -> a
 844   evalRHS 0 root actual = eval 0 root actual
 845
 846 It leads to the deferral of an equality
 847
 848   (String -> String -> String) ~ a
 849
 850 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
 851 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
 852 This has the *side effect* of also zonking the `a' in the deferred equality
 853 (which at this point is being handed around wrapped in an implication
 854 constraint).
 855
 856 Finally, the equality (with the zonked `a') will be handed back to the
 857 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
 858 If we zonk `a' with a regular type variable, we will have this regular type
 859 variable now floating around in the simplifier, which in many places assumes to
 860 only see proper TcTyVars.
 861
 862 We can avoid this problem by zonking with a skolem.  The skolem is rigid
 863 (which we requirefor a quantified variable), but is still a TcTyVar that the
 864 simplifier knows how to deal with.
 865
 866
 867 %************************************************************************
 868 %*                                                                      *
 869 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 870 %*                                                                      *
 871 %*              For internal use only!                                  *
 872 %*                                                                      *
 873 %************************************************************************
 874
 875 \begin{code}
 876 -- For unbound, mutable tyvars, zonkType uses the function given to it
 877 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 878 --      type variable and zonks the kind too
 879
 880 zonkType :: (TcTyVar -> TcM Type)       -- What to do with unbound mutable type variables
 881                                         -- see zonkTcType, and zonkTcTypeToType
 882          -> TcType
 883          -> TcM Type
 884 zonkType unbound_var_fn ty
 885   = go ty
 886   where
 887     go (TyConApp tc tys) = do tys' <- mapM go tys
 888                               return (TyConApp tc tys')
 889
 890     go (PredTy p)        = do p' <- go_pred p
 891                               return (PredTy p')
 892
 893     go (FunTy arg res)   = do arg' <- go arg
 894                               res' <- go res
 895                               return (FunTy arg' res')
 896
 897     go (AppTy fun arg)   = do fun' <- go fun
 898                               arg' <- go arg
 899                               return (mkAppTy fun' arg')
 900                 -- NB the mkAppTy; we might have instantiated a
 901                 -- type variable to a type constructor, so we need
 902                 -- to pull the TyConApp to the top.
 903
 904         -- The two interesting cases!
 905     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
 906                        | otherwise       = return (TyVarTy tyvar)
 907                 -- Ordinary (non Tc) tyvars occur inside quantified types
 908
 909     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
 910                              ty' <- go ty
 911                              return (ForAllTy tyvar ty')
 912
 913     go_pred (ClassP c tys)   = do tys' <- mapM go tys
 914                                   return (ClassP c tys')
 915     go_pred (IParam n ty)    = do ty' <- go ty
 916                                   return (IParam n ty')
 917     go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
 918                                   ty2' <- go ty2
 919                                   return (EqPred ty1' ty2')
 920
 921 zonk_tc_tyvar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variable
 922               -> TcTyVar -> TcM TcType
 923 zonk_tc_tyvar unbound_var_fn tyvar
 924   | not (isMetaTyVar tyvar)     -- Skolems
 925   = return (TyVarTy tyvar)
 926
 927   | otherwise                   -- Mutables
 928   = do  { cts <- readMetaTyVar tyvar
 929         ; case cts of
 930             Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
 931             Indirect ty -> zonkType unbound_var_fn ty  }
 932 \end{code}
 933
 934
 935
 936 %************************************************************************
 937 %*                                                                      *
 938                         Zonking kinds
 939 %*                                                                      *
 940 %************************************************************************
 941
 942 \begin{code}
 943 readKindVar  :: KindVar -> TcM (MetaDetails)
 944 writeKindVar :: KindVar -> TcKind -> TcM ()
 945 readKindVar  kv = readMutVar (kindVarRef kv)
 946 writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
 947
 948 -------------
 949 zonkTcKind :: TcKind -> TcM TcKind
 950 zonkTcKind k = zonkTcType k
 951
 952 -------------
 953 zonkTcKindToKind :: TcKind -> TcM Kind
 954 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
 955 -- Haskell specifies that * is to be used, so we follow that.
 956 zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
 957 \end{code}
 958
 959 %************************************************************************
 960 %*                                                                      *
 961 \subsection{Checking a user type}
 962 %*                                                                      *
 963 %************************************************************************
 964
 965 When dealing with a user-written type, we first translate it from an HsType
 966 to a Type, performing kind checking, and then check various things that should
 967 be true about it.  We don't want to perform these checks at the same time
 968 as the initial translation because (a) they are unnecessary for interface-file
 969 types and (b) when checking a mutually recursive group of type and class decls,
 970 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
 971 diverse, and used to really mess up the other code.
 972
 973 One thing we check for is 'rank'.
 974
 975         Rank 0:         monotypes (no foralls)
 976         Rank 1:         foralls at the front only, Rank 0 inside
 977         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 978
 979         basic ::= tyvar | T basic ... basic
 980
 981         r2  ::= forall tvs. cxt => r2a
 982         r2a ::= r1 -> r2a | basic
 983         r1  ::= forall tvs. cxt => r0
 984         r0  ::= r0 -> r0 | basic
 985
 986 Another thing is to check that type synonyms are saturated.
 987 This might not necessarily show up in kind checking.
 988         type A i = i
 989         data T k = MkT (k Int)
 990         f :: T A        -- BAD!
 991
 992
 993 \begin{code}
 994 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 995 -- Checks that the type is valid for the given context
 996 checkValidType ctxt ty = do
 997     traceTc (text "checkValidType" <+> ppr ty)
 998     unboxed  <- doptM Opt_UnboxedTuples
 999     rank2    <- doptM Opt_Rank2Types
1000     rankn    <- doptM Opt_RankNTypes
1001     polycomp <- doptM Opt_PolymorphicComponents
1002     let
1003         rank | rankn = Arbitrary
1004              | rank2 = Rank 2
1005              | otherwise
1006              = case ctxt of     -- Haskell 98
1007                  GenPatCtxt     -> Rank 0
1008                  LamPatSigCtxt  -> Rank 0
1009                  BindPatSigCtxt -> Rank 0
1010                  DefaultDeclCtxt-> Rank 0
1011                  ResSigCtxt     -> Rank 0
1012                  TySynCtxt _    -> Rank 0
1013                  ExprSigCtxt    -> Rank 1
1014                  FunSigCtxt _   -> Rank 1
1015                  ConArgCtxt _   -> if polycomp
1016                            then Rank 2
1017                                 -- We are given the type of the entire
1018                                 -- constructor, hence rank 1
1019                            else Rank 1
1020                  ForSigCtxt _   -> Rank 1
1021                  SpecInstCtxt   -> Rank 1
1022
1023         actual_kind = typeKind ty
1024
1025         kind_ok = case ctxt of
1026                         TySynCtxt _  -> True    -- Any kind will do
1027                         ResSigCtxt   -> isSubOpenTypeKind        actual_kind
1028                         ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
1029                         GenPatCtxt   -> isLiftedTypeKind actual_kind
1030                         ForSigCtxt _ -> isLiftedTypeKind actual_kind
1031                         other        -> isSubArgTypeKind    actual_kind
1032
1033         ubx_tup = case ctxt of
1034                       TySynCtxt _ | unboxed -> UT_Ok
1035                       ExprSigCtxt | unboxed -> UT_Ok
1036                       _                     -> UT_NotOk
1037
1038         -- Check that the thing has kind Type, and is lifted if necessary
1039     checkTc kind_ok (kindErr actual_kind)
1040
1041         -- Check the internal validity of the type itself
1042     check_type rank ubx_tup ty
1043
1044     traceTc (text "checkValidType done" <+> ppr ty)
1045
1046 checkValidMonoType :: Type -> TcM ()
1047 checkValidMonoType ty = check_mono_type ty
1048 \end{code}
1049
1050
1051 \begin{code}
1052 data Rank = Rank Int | Arbitrary
1053
1054 decRank :: Rank -> Rank
1055 decRank Arbitrary = Arbitrary
1056 decRank (Rank n)  = Rank (n-1)
1057
1058 nonZeroRank :: Rank -> Bool
1059 nonZeroRank (Rank 0) = False
1060 nonZeroRank _        = True
1061
1062 ----------------------------------------
1063 data UbxTupFlag = UT_Ok | UT_NotOk
1064         -- The "Ok" version means "ok if -fglasgow-exts is on"
1065
1066 ----------------------------------------
1067 check_mono_type :: Type -> TcM ()       -- No foralls anywhere
1068                                         -- No unlifted types of any kind
1069 check_mono_type ty
1070    = do { check_type (Rank 0) UT_NotOk ty
1071         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1072
1073 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
1074 -- The args say what the *type* context requires, independent
1075 -- of *flag* settings.  You test the flag settings at usage sites.
1076 --
1077 -- Rank is allowed rank for function args
1078 -- Rank 0 means no for-alls anywhere
1079
1080 check_type rank ubx_tup ty
1081   | not (null tvs && null theta)
1082   = do  { checkTc (nonZeroRank rank) (forAllTyErr ty)
1083                 -- Reject e.g. (Maybe (?x::Int => Int)),
1084                 -- with a decent error message
1085         ; check_valid_theta SigmaCtxt theta
1086         ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
1087         ; checkFreeness tvs theta
1088         ; checkAmbiguity tvs theta (tyVarsOfType tau) }
1089   where
1090     (tvs, theta, tau) = tcSplitSigmaTy ty
1091
1092 -- Naked PredTys don't usually show up, but they can as a result of
1093 --      {-# SPECIALISE instance Ord Char #-}
1094 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
1095 -- are handled, but the quick thing is just to permit PredTys here.
1096 check_type rank ubx_tup (PredTy sty)
1097   = do  { dflags <- getDOpts
1098         ; check_pred_ty dflags TypeCtxt sty }
1099
1100 check_type rank ubx_tup (TyVarTy _)       = return ()
1101 check_type rank ubx_tup ty@(FunTy arg_ty res_ty)
1102   = do  { check_type (decRank rank) UT_NotOk arg_ty
1103         ; check_type rank           UT_Ok    res_ty }
1104
1105 check_type rank ubx_tup (AppTy ty1 ty2)
1106   = do  { check_arg_type rank ty1
1107         ; check_arg_type rank ty2 }
1108
1109 check_type rank ubx_tup ty@(TyConApp tc tys)
1110   | isSynTyCon tc
1111   = do  {       -- Check that the synonym has enough args
1112                 -- This applies equally to open and closed synonyms
1113                 -- It's OK to have an *over-applied* type synonym
1114                 --      data Tree a b = ...
1115                 --      type Foo a = Tree [a]
1116                 --      f :: Foo a b -> ...
1117           checkTc (tyConArity tc <= length tys) arity_msg
1118
1119         -- See Note [Liberal type synonyms]
1120         ; liberal <- doptM Opt_LiberalTypeSynonyms
1121         ; if not liberal || isOpenSynTyCon tc then
1122                 -- For H98 and synonym families, do check the type args
1123                 mapM_ check_mono_type tys
1124
1125           else  -- In the liberal case (only for closed syns), expand then check
1126           case tcView ty of
1127              Just ty' -> check_type rank ubx_tup ty'
1128              Nothing  -> pprPanic "check_tau_type" (ppr ty)
1129     }
1130
1131   | isUnboxedTupleTyCon tc
1132   = do  { ub_tuples_allowed <- doptM Opt_UnboxedTuples
1133         ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
1134
1135         ; impred <- doptM Opt_ImpredicativeTypes
1136         ; let rank' = if impred then rank else Rank 0
1137                 -- c.f. check_arg_type
1138                 -- However, args are allowed to be unlifted, or
1139                 -- more unboxed tuples, so can't use check_arg_ty
1140         ; mapM_ (check_type rank' UT_Ok) tys }
1141
1142   | otherwise
1143   = mapM_ (check_arg_type rank) tys
1144
1145   where
1146     ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
1147
1148     n_args    = length tys
1149     tc_arity  = tyConArity tc
1150
1151     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
1152     ubx_tup_msg = ubxArgTyErr ty
1153
1154 ----------------------------------------
1155 check_arg_type :: Rank -> Type -> TcM ()
1156 -- The sort of type that can instantiate a type variable,
1157 -- or be the argument of a type constructor.
1158 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
1159 -- Other unboxed types are very occasionally allowed as type
1160 -- arguments depending on the kind of the type constructor
1161 --
1162 -- For example, we want to reject things like:
1163 --
1164 --      instance Ord a => Ord (forall s. T s a)
1165 -- and
1166 --      g :: T s (forall b.b)
1167 --
1168 -- NB: unboxed tuples can have polymorphic or unboxed args.
1169 --     This happens in the workers for functions returning
1170 --     product types with polymorphic components.
1171 --     But not in user code.
1172 -- Anyway, they are dealt with by a special case in check_tau_type
1173
1174 check_arg_type rank ty
1175   = do  { impred <- doptM Opt_ImpredicativeTypes
1176         ; let rank' = if impred then rank else Rank 0   -- Monotype unless impredicative
1177         ; check_type rank' UT_NotOk ty
1178         ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
1179
1180 ----------------------------------------
1181 forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
1182 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type:") <+> ppr ty
1183 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
1184 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
1185 \end{code}
1186
1187 Note [Liberal type synonyms]
1188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1189 If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
1190 doing validity checking.  This allows us to instantiate a synonym defn
1191 with a for-all type, or with a partially-applied type synonym.
1192         e.g.   type T a b = a
1193                type S m   = m ()
1194                f :: S (T Int)
1195 Here, T is partially applied, so it's illegal in H98.  But if you
1196 expand S first, then T we get just
1197                f :: Int
1198 which is fine.
1199
1200 IMPORTANT: suppose T is a type synonym.  Then we must do validity
1201 checking on an appliation (T ty1 ty2)
1202
1203         *either* before expansion (i.e. check ty1, ty2)
1204         *or* after expansion (i.e. expand T ty1 ty2, and then check)
1205         BUT NOT BOTH
1206
1207 If we do both, we get exponential behaviour!!
1208
1209   data TIACons1 i r c = c i ::: r c
1210   type TIACons2 t x = TIACons1 t (TIACons1 t x)
1211   type TIACons3 t x = TIACons2 t (TIACons1 t x)
1212   type TIACons4 t x = TIACons2 t (TIACons2 t x)
1213   type TIACons7 t x = TIACons4 t (TIACons3 t x)
1214
1215
1216 %************************************************************************
1217 %*                                                                      *
1218 \subsection{Checking a theta or source type}
1219 %*                                                                      *
1220 %************************************************************************
1221
1222 \begin{code}
1223 -- Enumerate the contexts in which a "source type", <S>, can occur
1224 --      Eq a
1225 -- or   ?x::Int
1226 -- or   r <: {x::Int}
1227 -- or   (N a) where N is a newtype
1228
1229 data SourceTyCtxt
1230   = ClassSCCtxt Name    -- Superclasses of clas
1231                         --      class <S> => C a where ...
1232   | SigmaCtxt           -- Theta part of a normal for-all type
1233                         --      f :: <S> => a -> a
1234   | DataTyCtxt Name     -- Theta part of a data decl
1235                         --      data <S> => T a = MkT a
1236   | TypeCtxt            -- Source type in an ordinary type
1237                         --      f :: N a -> N a
1238   | InstThetaCtxt       -- Context of an instance decl
1239                         --      instance <S> => C [a] where ...
1240
1241 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
1242 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
1243 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
1244 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
1245 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
1246 \end{code}
1247
1248 \begin{code}
1249 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
1250 checkValidTheta ctxt theta
1251   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
1252
1253 -------------------------
1254 check_valid_theta ctxt []
1255   = return ()
1256 check_valid_theta ctxt theta = do
1257     dflags <- getDOpts
1258     warnTc (notNull dups) (dupPredWarn dups)
1259     mapM_ (check_pred_ty dflags ctxt) theta
1260   where
1261     (_,dups) = removeDups tcCmpPred theta
1262
1263 -------------------------
1264 check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
1265 check_pred_ty dflags ctxt pred@(ClassP cls tys)
1266   = do {        -- Class predicates are valid in all contexts
1267        ; checkTc (arity == n_tys) arity_err
1268
1269                 -- Check the form of the argument types
1270        ; mapM_ check_mono_type tys
1271        ; checkTc (check_class_pred_tys dflags ctxt tys)
1272                  (predTyVarErr pred $$ how_to_allow)
1273        }
1274   where
1275     class_name = className cls
1276     arity      = classArity cls
1277     n_tys      = length tys
1278     arity_err  = arityErr "Class" class_name arity n_tys
1279     how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
1280
1281 check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
1282   = do {        -- Equational constraints are valid in all contexts if type
1283                 -- families are permitted
1284        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
1285
1286                 -- Check the form of the argument types
1287        ; check_mono_type ty1
1288        ; check_mono_type ty2
1289        }
1290
1291 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
1292         -- Implicit parameters only allowed in type
1293         -- signatures; not in instance decls, superclasses etc
1294         -- The reason for not allowing implicit params in instances is a bit
1295         -- subtle.
1296         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
1297         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
1298         -- discharge all the potential usas of the ?x in e.   For example, a
1299         -- constraint Foo [Int] might come out of e,and applying the
1300         -- instance decl would show up two uses of ?x.
1301
1302 -- Catch-all
1303 check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
1304
1305 -------------------------
1306 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
1307 check_class_pred_tys dflags ctxt tys
1308   = case ctxt of
1309         TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
1310         InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
1311                                 -- Further checks on head and theta in
1312                                 -- checkInstTermination
1313         other         -> flexible_contexts || all tyvar_head tys
1314   where
1315     flexible_contexts = dopt Opt_FlexibleContexts dflags
1316     undecidable_ok = dopt Opt_UndecidableInstances dflags
1317
1318 -------------------------
1319 tyvar_head ty                   -- Haskell 98 allows predicates of form
1320   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
1321   | otherwise                   -- where a is a type variable
1322   = case tcSplitAppTy_maybe ty of
1323         Just (ty, _) -> tyvar_head ty
1324         Nothing      -> False
1325 \end{code}
1326
1327 Check for ambiguity
1328 ~~~~~~~~~~~~~~~~~~~
1329           forall V. P => tau
1330 is ambiguous if P contains generic variables
1331 (i.e. one of the Vs) that are not mentioned in tau
1332
1333 However, we need to take account of functional dependencies
1334 when we speak of 'mentioned in tau'.  Example:
1335         class C a b | a -> b where ...
1336 Then the type
1337         forall x y. (C x y) => x
1338 is not ambiguous because x is mentioned and x determines y
1339
1340 NB; the ambiguity check is only used for *user* types, not for types
1341 coming from inteface files.  The latter can legitimately have
1342 ambiguous types. Example
1343
1344    class S a where s :: a -> (Int,Int)
1345    instance S Char where s _ = (1,1)
1346    f:: S a => [a] -> Int -> (Int,Int)
1347    f (_::[a]) x = (a*x,b)
1348         where (a,b) = s (undefined::a)
1349
1350 Here the worker for f gets the type
1351         fw :: forall a. S a => Int -> (# Int, Int #)
1352
1353 If the list of tv_names is empty, we have a monotype, and then we
1354 don't need to check for ambiguity either, because the test can't fail
1355 (see is_ambig).
1356
1357
1358 \begin{code}
1359 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
1360 checkAmbiguity forall_tyvars theta tau_tyvars
1361   = mapM_ complain (filter is_ambig theta)
1362   where
1363     complain pred     = addErrTc (ambigErr pred)
1364     extended_tau_vars = grow theta tau_tyvars
1365
1366         -- See Note [Implicit parameters and ambiguity] in TcSimplify
1367     is_ambig pred     = isClassPred  pred &&
1368                         any ambig_var (varSetElems (tyVarsOfPred pred))
1369
1370     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
1371                         not (ct_var `elemVarSet` extended_tau_vars)
1372
1373 ambigErr pred
1374   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
1375          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
1376                  ptext SLIT("must be reachable from the type after the '=>'"))]
1377 \end{code}
1378
1379 In addition, GHC insists that at least one type variable
1380 in each constraint is in V.  So we disallow a type like
1381         forall a. Eq b => b -> b
1382 even in a scope where b is in scope.
1383
1384 \begin{code}
1385 checkFreeness forall_tyvars theta
1386   = do  { flexible_contexts <- doptM Opt_FlexibleContexts
1387         ; unless flexible_contexts $ mapM_ complain (filter is_free theta) }
1388   where
1389     is_free pred     =  not (isIPPred pred)
1390                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
1391     bound_var ct_var = ct_var `elem` forall_tyvars
1392     complain pred    = addErrTc (freeErr pred)
1393
1394 freeErr pred
1395   = sep [ ptext SLIT("All of the type variables in the constraint") <+>
1396           quotes (pprPred pred)
1397         , ptext SLIT("are already in scope") <+>
1398           ptext SLIT("(at least one must be universally quantified here)")
1399         , nest 4 $
1400             ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
1401         ]
1402 \end{code}
1403
1404 \begin{code}
1405 checkThetaCtxt ctxt theta
1406   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
1407           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
1408
1409 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
1410 eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
1411                    $$
1412                    parens (ptext SLIT("Use -XTypeFamilies to permit this"))
1413 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
1414                           nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1415 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
1416
1417 arityErr kind name n m
1418   = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
1419            n_arguments <> comma, text "but has been given", int m]
1420     where
1421         n_arguments | n == 0 = ptext SLIT("no arguments")
1422                     | n == 1 = ptext SLIT("1 argument")
1423                     | True   = hsep [int n, ptext SLIT("arguments")]
1424
1425 -----------------
1426 notMonoType ty
1427   = do  { ty' <- zonkTcType ty
1428         ; env0 <- tcInitTidyEnv
1429         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1430               msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
1431         ; failWithTcM (env1, msg) }
1432
1433 notMonoArgs ty
1434   = do  { ty' <- zonkTcType ty
1435         ; env0 <- tcInitTidyEnv
1436         ; let (env1, tidy_ty) = tidyOpenType env0 ty'
1437               msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
1438         ; failWithTcM (env1, msg) }
1439 \end{code}
1440
1441
1442 %************************************************************************
1443 %*                                                                      *
1444 \subsection{Checking for a decent instance head type}
1445 %*                                                                      *
1446 %************************************************************************
1447
1448 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
1449 it must normally look like: @instance Foo (Tycon a b c ...) ...@
1450
1451 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
1452 flag is on, or (2)~the instance is imported (they must have been
1453 compiled elsewhere). In these cases, we let them go through anyway.
1454
1455 We can also have instances for functions: @instance Foo (a -> b) ...@.
1456
1457 \begin{code}
1458 checkValidInstHead :: Type -> TcM (Class, [TcType])
1459
1460 checkValidInstHead ty   -- Should be a source type
1461   = case tcSplitPredTy_maybe ty of {
1462         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
1463         Just pred ->
1464
1465     case getClassPredTys_maybe pred of {
1466         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
1467         Just (clas,tys) -> do
1468
1469     dflags <- getDOpts
1470     mapM_ check_mono_type tys
1471     check_inst_head dflags clas tys
1472     return (clas, tys)
1473     }}
1474
1475 check_inst_head dflags clas tys
1476         -- If GlasgowExts then check at least one isn't a type variable
1477   = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
1478                 all tcInstHeadTyNotSynonym tys)
1479                (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
1480        checkTc (dopt Opt_FlexibleInstances dflags ||
1481                 all tcInstHeadTyAppAllTyVars tys)
1482                (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
1483        checkTc (dopt Opt_MultiParamTypeClasses dflags ||
1484                 isSingleton tys)
1485                (instTypeErr (pprClassPred clas tys) head_one_type_msg)
1486        mapM_ check_mono_type tys
1487         -- For now, I only allow tau-types (not polytypes) in
1488         -- the head of an instance decl.
1489         --      E.g.  instance C (forall a. a->a) is rejected
1490         -- One could imagine generalising that, but I'm not sure
1491         -- what all the consequences might be
1492
1493   where
1494     head_type_synonym_msg = parens (
1495                 text "All instance types must be of the form (T t1 ... tn)" $$
1496                 text "where T is not a synonym." $$
1497                 text "Use -XTypeSynonymInstances if you want to disable this.")
1498
1499     head_type_args_tyvars_msg = parens (vcat [
1500                 text "All instance types must be of the form (T a1 ... an)",
1501                 text "where a1 ... an are type *variables*,",
1502                 text "and each type variable appears at most once in the instance head.",
1503                 text "Use -XFlexibleInstances if you want to disable this."])
1504
1505     head_one_type_msg = parens (
1506                 text "Only one type can be given in an instance head." $$
1507                 text "Use -XMultiParamTypeClasses if you want to allow more.")
1508
1509 instTypeErr pp_ty msg
1510   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
1511          nest 4 msg]
1512 \end{code}
1513
1514
1515 %************************************************************************
1516 %*                                                                      *
1517 \subsection{Checking instance for termination}
1518 %*                                                                      *
1519 %************************************************************************
1520
1521
1522 \begin{code}
1523 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
1524 checkValidInstance tyvars theta clas inst_tys
1525   = do  { undecidable_ok <- doptM Opt_UndecidableInstances
1526
1527         ; checkValidTheta InstThetaCtxt theta
1528         ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
1529
1530         -- Check that instance inference will terminate (if we care)
1531         -- For Haskell 98 this will already have been done by checkValidTheta,
1532         -- but as we may be using other extensions we need to check.
1533         ; unless undecidable_ok $
1534           mapM_ addErrTc (checkInstTermination inst_tys theta)
1535
1536         -- The Coverage Condition
1537         ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
1538                   (instTypeErr (pprClassPred clas inst_tys) msg)
1539         }
1540   where
1541     msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
1542                          undecidableMsg])
1543 \end{code}
1544
1545 Termination test: the so-called "Paterson conditions" (see Section 5 of
1546 "Understanding functionsl dependencies via Constraint Handling Rules,
1547 JFP Jan 2007).
1548
1549 We check that each assertion in the context satisfies:
1550  (1) no variable has more occurrences in the assertion than in the head, and
1551  (2) the assertion has fewer constructors and variables (taken together
1552      and counting repetitions) than the head.
1553 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
1554 (which have already been checked) guarantee termination.
1555
1556 The underlying idea is that
1557
1558     for any ground substitution, each assertion in the
1559     context has fewer type constructors than the head.
1560
1561
1562 \begin{code}
1563 checkInstTermination :: [TcType] -> ThetaType -> [Message]
1564 checkInstTermination tys theta
1565   = mapCatMaybes check theta
1566   where
1567    fvs  = fvTypes tys
1568    size = sizeTypes tys
1569    check pred
1570       | not (null (fvPred pred \\ fvs))
1571       = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
1572       | sizePred pred >= size
1573       = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
1574       | otherwise
1575       = Nothing
1576
1577 predUndecErr pred msg = sep [msg,
1578                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
1579
1580 nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
1581 smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
1582 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1583 \end{code}
1584
1585
1586 %************************************************************************
1587 %*                                                                      *
1588         Checking the context of a derived instance declaration
1589 %*                                                                      *
1590 %************************************************************************
1591
1592 Note [Exotic derived instance contexts]
1593 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1594 In a 'derived' instance declaration, we *infer* the context.  It's a
1595 bit unclear what rules we should apply for this; the Haskell report is
1596 silent.  Obviously, constraints like (Eq a) are fine, but what about
1597         data T f a = MkT (f a) deriving( Eq )
1598 where we'd get an Eq (f a) constraint.  That's probably fine too.
1599
1600 One could go further: consider
1601         data T a b c = MkT (Foo a b c) deriving( Eq )
1602         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
1603
1604 Notice that this instance (just) satisfies the Paterson termination
1605 conditions.  Then we *could* derive an instance decl like this:
1606
1607         instance (C Int a, Eq b, Eq c) => Eq (T a b c)
1608
1609 even though there is no instance for (C Int a), because there just
1610 *might* be an instance for, say, (C Int Bool) at a site where we
1611 need the equality instance for T's.
1612
1613 However, this seems pretty exotic, and it's quite tricky to allow
1614 this, and yet give sensible error messages in the (much more common)
1615 case where we really want that instance decl for C.
1616
1617 So for now we simply require that the derived instance context
1618 should have only type-variable constraints.
1619
1620 Here is another example:
1621         data Fix f = In (f (Fix f)) deriving( Eq )
1622 Here, if we are prepared to allow -fallow-undecidable-instances we
1623 could derive the instance
1624         instance Eq (f (Fix f)) => Eq (Fix f)
1625 but this is so delicate that I don't think it should happen inside
1626 'deriving'. If you want this, write it yourself!
1627
1628 NB: if you want to lift this condition, make sure you still meet the
1629 termination conditions!  If not, the deriving mechanism generates
1630 larger and larger constraints.  Example:
1631   data Succ a = S a
1632   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
1633
1634 Note the lack of a Show instance for Succ.  First we'll generate
1635   instance (Show (Succ a), Show a) => Show (Seq a)
1636 and then
1637   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
1638 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
1639
1640 The bottom line
1641 ~~~~~~~~~~~~~~~
1642 Allow constraints which consist only of type variables, with no repeats.
1643
1644 \begin{code}
1645 validDerivPred :: PredType -> Bool
1646 validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
1647                                 where fvs = fvTypes tys
1648 validDerivPred otehr            = False
1649 \end{code}
1650
1651 %************************************************************************
1652 %*                                                                      *
1653         Checking type instance well-formedness and termination
1654 %*                                                                      *
1655 %************************************************************************
1656
1657 \begin{code}
1658 -- Check that a "type instance" is well-formed (which includes decidability
1659 -- unless -fallow-undecidable-instances is given).
1660 --
1661 checkValidTypeInst :: [Type] -> Type -> TcM ()
1662 checkValidTypeInst typats rhs
1663   = do { -- left-hand side contains no type family applications
1664          -- (vanilla synonyms are fine, though)
1665        ; mapM_ checkTyFamFreeness typats
1666
1667          -- the right-hand side is a tau type
1668        ; checkTc (isTauTy rhs) $
1669            polyTyErr rhs
1670
1671          -- we have a decidable instance unless otherwise permitted
1672        ; undecidable_ok <- doptM Opt_UndecidableInstances
1673        ; unless undecidable_ok $
1674            mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
1675        }
1676
1677 -- Make sure that each type family instance is
1678 --   (1) strictly smaller than the lhs,
1679 --   (2) mentions no type variable more often than the lhs, and
1680 --   (3) does not contain any further type family instances.
1681 --
1682 checkFamInst :: [Type]                  -- lhs
1683              -> [(TyCon, [Type])]       -- type family instances
1684              -> [Message]
1685 checkFamInst lhsTys famInsts
1686   = mapCatMaybes check famInsts
1687   where
1688    size = sizeTypes lhsTys
1689    fvs  = fvTypes lhsTys
1690    check (tc, tys)
1691       | not (all isTyFamFree tys)
1692       = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
1693       | not (null (fvTypes tys \\ fvs))
1694       = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
1695       | size <= sizeTypes tys
1696       = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
1697       | otherwise
1698       = Nothing
1699       where
1700         famInst = TyConApp tc tys
1701
1702 -- Ensure that no type family instances occur in a type.
1703 --
1704 checkTyFamFreeness :: Type -> TcM ()
1705 checkTyFamFreeness ty
1706   = checkTc (isTyFamFree ty) $
1707       tyFamInstInIndexErr ty
1708
1709 -- Check that a type does not contain any type family applications.
1710 --
1711 isTyFamFree :: Type -> Bool
1712 isTyFamFree = null . tyFamInsts
1713
1714 -- Error messages
1715
1716 tyFamInstInIndexErr ty
1717   = hang (ptext SLIT("Illegal type family application in type instance") <>
1718          colon) 4 $
1719       ppr ty
1720
1721 polyTyErr ty
1722   = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
1723       ppr ty
1724
1725 famInstUndecErr ty msg
1726   = sep [msg,
1727          nest 2 (ptext SLIT("in the type family application:") <+>
1728                  pprType ty)]
1729
1730 nestedMsg     = ptext SLIT("Nested type family application")
1731 nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
1732 smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
1733 \end{code}
1734
1735
1736 %************************************************************************
1737 %*                                                                      *
1738 \subsection{Auxiliary functions}
1739 %*                                                                      *
1740 %************************************************************************
1741
1742 \begin{code}
1743 -- Free variables of a type, retaining repetitions, and expanding synonyms
1744 fvType :: Type -> [TyVar]
1745 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
1746 fvType (TyVarTy tv)        = [tv]
1747 fvType (TyConApp _ tys)    = fvTypes tys
1748 fvType (PredTy pred)       = fvPred pred
1749 fvType (FunTy arg res)     = fvType arg ++ fvType res
1750 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
1751 fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
1752
1753 fvTypes :: [Type] -> [TyVar]
1754 fvTypes tys                = concat (map fvType tys)
1755
1756 fvPred :: PredType -> [TyVar]
1757 fvPred (ClassP _ tys')     = fvTypes tys'
1758 fvPred (IParam _ ty)       = fvType ty
1759 fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
1760
1761 -- Size of a type: the number of variables and constructors
1762 sizeType :: Type -> Int
1763 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
1764 sizeType (TyVarTy _)       = 1
1765 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
1766 sizeType (PredTy pred)     = sizePred pred
1767 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
1768 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
1769 sizeType (ForAllTy _ ty)   = sizeType ty
1770
1771 sizeTypes :: [Type] -> Int
1772 sizeTypes xs               = sum (map sizeType xs)
1773
1774 sizePred :: PredType -> Int
1775 sizePred (ClassP _ tys')   = sizeTypes tys'
1776 sizePred (IParam _ ty)     = sizeType ty
1777 sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
1778 \end{code}