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