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