diff options
| author | sheaf <sam.derbyshire@gmail.com> | 2022-07-22 13:29:49 +0200 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-07-25 09:43:58 -0400 |
| commit | c24ca5c3b1246465f5fee4388effba74ea5351ad (patch) | |
| tree | 21cd12a8098e61a58c887f6beda4d0a5c44b9b6f | |
| parent | 73836fc84b6b39fed34ccb3a501f7a88658c1400 (diff) | |
| download | haskell-c24ca5c3b1246465f5fee4388effba74ea5351ad.tar.gz | |
Docs: clarify ConstraintKinds infelicity
GHC doesn't consistently require the ConstraintKinds extension to
be enabled, as it allows programs such as type families returning
a constraint without this extension.
MR !7784 fixes this infelicity, but breaking user programs was deemed
to not be worth it, so we document it instead.
Fixes #21061.
| -rw-r--r-- | docs/users_guide/exts/constraint_kind.rst | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/docs/users_guide/exts/constraint_kind.rst b/docs/users_guide/exts/constraint_kind.rst index 9077e25ce3..fd51e17859 100644 --- a/docs/users_guide/exts/constraint_kind.rst +++ b/docs/users_guide/exts/constraint_kind.rst @@ -35,19 +35,27 @@ The following things have kind ``Constraint``: - Anything whose form is not yet known, but the user has declared to have kind ``Constraint`` (for which they need to import it from - ``Data.Kind``). So for example + ``Data.Kind``). For example ``type Foo (f :: Type -> Constraint) = forall b. f b => b -> b`` - is allowed, as well as examples involving type families: :: + is allowed. - type family Typ a b :: Constraint - type instance Typ Int b = Show b - type instance Typ Bool b = Num b +Note, however, that the :extension:`TypeFamilies` and :extension:`GADTs` extensions +also allow the manipulation of things with kind ``Constraint``, without necessarily +requiring the :extension:`ConstraintKinds` extension: :: - func :: Typ a b => a -> b -> b - func = ... + -- With -XTypeFamilies -XNoConstraintKinds + type T :: Type -> (Type -> Constraint) + type family T a where + T Int = Num + T Double = Floating -Note that because constraints are just handled as types of a particular -kind, this extension allows type constraint synonyms: :: + -- With -XGADTs -XNoConstraintKinds + type Dict :: Constraint -> Type + data Dict c where + MkDict :: c => Dict c + +With the :extension:`ConstraintKinds` extension, constraints are just handled as +types of a particular kind. This allows type constraint synonyms: :: type Stringy a = (Read a, Show a) foo :: Stringy a => a -> (String, String -> a) @@ -77,5 +85,3 @@ You may write programs that use exotic sorts of constraints in instance contexts and superclasses, but to do so you must use :extension:`UndecidableInstances` to signal that you don't mind if the type checker fails to terminate. - - |