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