Updated documentation; changed "group" to "branched" in type families
[ghc.git] / compiler / types / Kind.lhs
index 2bdabc6..0082a33 100644 (file)
@@ -1,68 +1,66 @@
 %
-% (c) The University of Glasgow 2006
+% (c) The University of Glasgow 2006-2012
 %
 
 \begin{code}
+{-# OPTIONS -fno-warn-tabs #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and
+-- detab the module (please do the detabbing in a separate patch). See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
+-- for details
+
 module Kind (
         -- * Main data type
-        Kind, typeKind,
+        SuperKind, Kind, typeKind,
 
        -- Kinds
-       liftedTypeKind, unliftedTypeKind, openTypeKind,
-        argTypeKind, ubxTupleKind, constraintKind,
+       anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind,
         mkArrowKind, mkArrowKinds,
 
         -- Kind constructors...
-        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
-        argTypeKindTyCon, ubxTupleKindTyCon, constraintKindTyCon,
+        anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
+        unliftedTypeKindTyCon, constraintKindTyCon,
 
         -- Super Kinds
-       tySuperKind, tySuperKindTyCon, 
+       superKind, superKindTyCon, 
         
        pprKind, pprParendKind,
 
         -- ** Deconstructing Kinds
-        kindFunResult, kindAppResult, synTyConResKind,
+        kindAppResult, synTyConResKind,
         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
-        isUbxTupleKind, isArgTypeKind, isConstraintKind, isKind, isTySuperKind,
-        isSuperKind, 
+        isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind,
+        isKind, isKindVar,
+        isSuperKind, isSuperKindTyCon,
         isLiftedTypeKindCon, isConstraintKindCon,
+        isAnyKind, isAnyKindCon,
+        okArrowArgKind, okArrowResultKind,
+
+        isSubOpenTypeKind, 
+        isSubKind, isSubKindCon, 
+        tcIsSubKind, tcIsSubKindCon,
+        defaultKind,
 
-        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
-        isSubKindCon,
+        -- ** Functions on variables
+        kiVarsOfKind, kiVarsOfKinds
 
        ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} Type (typeKind)
+import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
 
 import TypeRep
 import TysPrim
 import TyCon
+import VarSet
 import PrelNames
 import Outputable
-\end{code}
-
-%************************************************************************
-%*                                                                     *
-        Predicates over Kinds
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-isTySuperKind :: SuperKind -> Bool
-isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
-isTySuperKind _                = False
-
--------------------
--- Lastly we need a few functions on Kinds
-
-isLiftedTypeKindCon :: TyCon -> Bool
-isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
+import Util
 \end{code}
 
 %************************************************************************
@@ -71,15 +69,40 @@ isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
 %*                                                                     *
 %************************************************************************
 
+Note [Kind Constraint and kind *]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The kind Constraint is the kind of classes and other type constraints.
+The special thing about types of kind Constraint is that 
+ * They are displayed with double arrow:
+     f :: Ord a => a -> a
+ * They are implicitly instantiated at call sites; so the type inference
+   engine inserts an extra argument of type (Ord a) at every call site
+   to f.
+
+However, once type inference is over, there is *no* distinction between 
+Constraint and *.  Indeed we can have coercions between the two. Consider
+   class C a where
+     op :: a -> a
+For this single-method class we may generate a newtype, which in turn 
+generates an axiom witnessing
+    Ord a ~ (a -> a)
+so on the left we have Constraint, and on the right we have *.
+See Trac #7451.
+
+Bottom line: although '*' and 'Constraint' are distinct TyCons, with
+distinct uniques, they are treated as equal at all times except 
+during type inference.  Hence cmpTc treats them as equal.
+
 \begin{code}
--- | Essentially 'funResultTy' on kinds
-kindFunResult :: Kind -> Kind
-kindFunResult (FunTy _ res) = res
-kindFunResult k = pprPanic "kindFunResult" (ppr k)
+-- | Essentially 'funResultTy' on kinds handling pi-types too
+kindFunResult :: Kind -> KindOrType -> Kind
+kindFunResult (FunTy _ res) _ = res
+kindFunResult (ForAllTy kv res) arg = substKiWith [kv] [arg] res
+kindFunResult k _ = pprPanic "kindFunResult" (ppr k)
 
-kindAppResult :: Kind -> [arg] -> Kind
+kindAppResult :: Kind -> [Type] -> Kind
 kindAppResult k []     = k
-kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
+kindAppResult k (a:as) = kindAppResult (kindFunResult k a) as
 
 -- | Essentially 'splitFunTys' on kinds
 splitKindFunTys :: Kind -> ([Kind],Kind)
@@ -103,65 +126,86 @@ splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
 -- Actually this function works fine on data types too, 
 -- but they'd always return '*', so we never need to ask
 synTyConResKind :: TyCon -> Kind
-synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
+synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
 
 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
-isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind, isConstraintKind :: Kind -> Bool
-isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
-        isUnliftedTypeKindCon, isSubArgTypeKindCon, isConstraintKindCon      :: TyCon -> Bool
+isOpenTypeKind, isUnliftedTypeKind,
+  isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
 
-isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
+isOpenTypeKindCon, isUnliftedTypeKindCon,
+  isSubOpenTypeKindCon, isConstraintKindCon,
+  isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool
 
-isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
-isOpenTypeKind _               = False
-
-isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
 
-isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
-isUbxTupleKind _               = False
-
-isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
+isLiftedTypeKindCon   tc = tyConUnique tc == liftedTypeKindTyConKey
+isAnyKindCon          tc = tyConUnique tc == anyKindTyConKey
+isOpenTypeKindCon     tc = tyConUnique tc == openTypeKindTyConKey
+isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+isConstraintKindCon   tc = tyConUnique tc == constraintKindTyConKey
+isSuperKindTyCon      tc = tyConUnique tc == superKindTyConKey
 
-isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
-isArgTypeKind _               = False
+isAnyKind (TyConApp tc _) = isAnyKindCon tc
+isAnyKind _               = False
 
-isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
+isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
+isOpenTypeKind _               = False
 
 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
 isUnliftedTypeKind _               = False
 
-isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
-
 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
 isConstraintKind _               = False
 
-isSubOpenTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
-isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
-                                     ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
-                                     False
-isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
-isSubOpenTypeKind other            = ASSERT( isKind other ) False
-         -- This is a conservative answer
-         -- It matters in the call to isSubKind in
-        -- checkExpectedKind.
-
-isSubArgTypeKindCon kc
+isConstraintOrLiftedKind (TyConApp tc _)
+  = isConstraintKindCon tc || isLiftedTypeKindCon tc
+isConstraintOrLiftedKind _ = False
+
+returnsConstraintKind :: Kind -> Bool
+returnsConstraintKind (ForAllTy _ k)  = returnsConstraintKind k
+returnsConstraintKind (FunTy _ k)     = returnsConstraintKind k
+returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
+returnsConstraintKind _               = False
+
+--------------------------------------------
+--            Kinding for arrow (->)
+-- Says when a kind is acceptable on lhs or rhs of an arrow
+--     arg -> res
+
+okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool
+okArrowArgKindCon kc
+  | isLiftedTypeKindCon   kc = True
   | isUnliftedTypeKindCon kc = True
-  | isLiftedTypeKindCon kc   = True
-  | isArgTypeKindCon kc      = True
-  | isConstraintKindCon kc   = True
+  | isConstraintKindCon   kc = True
   | otherwise                = False
 
-isSubArgTypeKind :: Kind -> Bool
--- ^ True of any sub-kind of ArgTypeKind 
-isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
-isSubArgTypeKind _                = False
+okArrowResultKindCon = okArrowArgKindCon
+
+okArrowArgKind, okArrowResultKind :: Kind -> Bool
+okArrowArgKind    (TyConApp kc []) = okArrowArgKindCon kc
+okArrowArgKind    _                = False
 
--- | Is this a super-kind (i.e. a type-of-kinds)?
-isSuperKind :: Type -> Bool
-isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
-isSuperKind _                   = False
+okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc
+okArrowResultKind _                = False
+
+-----------------------------------------
+--              Subkinding
+-- The tc variants are used during type-checking, where we don't want the
+-- Constraint kind to be a subkind of anything
+-- After type-checking (in core), Constraint is a subkind of openTypeKind
+
+isSubOpenTypeKind :: Kind -> Bool
+-- ^ True of any sub-kind of OpenTypeKind
+isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
+isSubOpenTypeKind _                = False
+
+isSubOpenTypeKindCon kc
+  =  isOpenTypeKindCon   kc
+  || isUnliftedTypeKindCon kc
+  || isLiftedTypeKindCon   kc  
+  || isConstraintKindCon kc   -- Needed for error (Num a) "blah"
+                              -- and so that (Ord a -> Eq a) is well-kinded
+                              -- and so that (# Eq a, Ord b #) is well-kinded
+                              -- See Note [Kind Constraint and kind *]
 
 -- | Is this a kind (i.e. a type-of-types)?
 isKind :: Kind -> Bool
@@ -169,25 +213,67 @@ isKind k = isSuperKind (typeKind k)
 
 isSubKind :: Kind -> Kind -> Bool
 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
-isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
-isSubKind (FunTy a1 r1) (FunTy a2 r2)        = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
-isSubKind _             _                     = False
+-- Sub-kinding is extremely simple and does not look
+-- under arrrows or type constructors
+
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
+isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
+  | isPromotedTyCon kc1 || isPromotedTyCon kc2
+    -- handles promoted kinds (List *, Nat, etc.)
+  = eqKind k1 k2
+
+  | otherwise -- handles usual kinds (*, #, (#), etc.)
+  = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
+    kc1 `isSubKindCon` kc2
+
+isSubKind k1 k2 = eqKind k1 k2
 
 isSubKindCon :: TyCon -> TyCon -> Bool
 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
-isSubKindCon kc1 kc2
-  | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
-  | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
-  | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
-  | isConstraintKindCon kc1   && isConstraintKindCon kc2   = True
-  | isOpenTypeKindCon kc2                                  = True 
-                           -- we already know kc1 is not a fun, its a TyCon
-  | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
-  | otherwise                                              = False
 
+-- If you edit this function, you may need to update the GHC formalism
+-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
+isSubKindCon kc1 kc2
+  | kc1 == kc2              = True
+  | isOpenTypeKindCon kc2   = isSubOpenTypeKindCon kc1 
+  | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2
+  | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2
+    -- See Note [Kind Constraint and kind *]
+  | otherwise               = False
+
+-------------------------
+-- Hack alert: we need a tiny variant for the typechecker
+-- Reason:     f :: Int -> (a~b)
+--             g :: forall (c::Constraint). Int -> c
+--             h :: Int => Int
+-- We want to reject these, even though Constraint is
+-- a sub-kind of OpenTypeKind.  It must be a sub-kind of OpenTypeKind
+-- *after* the typechecker
+--   a) So that (Ord a -> Eq a) is a legal type
+--   b) So that the simplifer can generate (error (Eq a) "urk")
+-- Moreover, after the type checker, Constraint and *
+-- are identical; see Note [Kind Constraint and kind *]
+--
+-- Easiest way to reject is simply to make Constraint a compliete
+-- below OpenTypeKind when type checking
+
+tcIsSubKind :: Kind -> Kind -> Bool
+tcIsSubKind k1 k2
+  | isConstraintKind k1 = isConstraintKind k2
+  | isConstraintKind k2 = isConstraintKind k1
+  | otherwise           = isSubKind k1 k2
+
+tcIsSubKindCon :: TyCon -> TyCon -> Bool
+tcIsSubKindCon kc1 kc2
+  | isConstraintKindCon kc1 = isConstraintKindCon kc2
+  | isConstraintKindCon kc2 = isConstraintKindCon kc1
+  | otherwise               = isSubKindCon kc1 kc2
+
+-------------------------
 defaultKind :: Kind -> Kind
--- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
--- information on what that means
+-- ^ Used when generalising: default OpenKind and ArgKind to *.
+-- See "Type#kind_subtyping" for more information on what that means
 
 -- When we generalise, we make generic type variables whose kind is
 -- simple (* or *->* etc).  So generic type variables (other than
@@ -197,11 +283,20 @@ defaultKind :: Kind -> Kind
 -- We want f to get type
 --     f :: forall (a::*). a -> Bool
 -- Not 
---     f :: forall (a::??). a -> Bool
+--     f :: forall (a::ArgKind). a -> Bool
 -- because that would allow a call like (f 3#) as well as (f True),
---and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
-defaultKind k 
-  | isSubOpenTypeKind k = liftedTypeKind
-  | isSubArgTypeKind k  = liftedTypeKind
-  | otherwise        = k
-\end{code}
\ No newline at end of file
+-- and the calling conventions differ.
+-- This defaulting is done in TcMType.zonkTcTyVarBndr.
+--
+-- The test is really whether the kind is strictly above '*'
+defaultKind (TyConApp kc _args)
+  | isOpenTypeKindCon kc = ASSERT( null _args ) liftedTypeKind
+defaultKind k = k
+
+-- Returns the free kind variables in a kind
+kiVarsOfKind :: Kind -> VarSet
+kiVarsOfKind = tyVarsOfType
+
+kiVarsOfKinds :: [Kind] -> VarSet
+kiVarsOfKinds = tyVarsOfTypes
+\end{code}