GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:39Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11381Put injective type families in a separate language extension2019-07-07T18:30:39ZJan Stolarekjan.stolarek@ed.ac.ukPut injective type families in a separate language extensionInjective type families should only be enabled when language extension `TypeFamilyDependencies` is specified. This extension should imply `TypeFamilies`.Injective type families should only be enabled when language extension `TypeFamilyDependencies` is specified. This extension should imply `TypeFamilies`.8.0.1Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/6018Injective type families2019-07-07T18:52:33ZlunarisInjective type familiesInjective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
I've naively attempted a proof-of-concept in GHC. It's almost certainly incorrect and probably breaks the type...Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
I've naively attempted a proof-of-concept in GHC. It's almost certainly incorrect and probably breaks the type system, but I thought it best to put it here and see if it can be made workable.
In summary, my changes are:
- Add a new keyword, `injective`, which is available only when the `TypeFamilies` extension is enabled. Injective families may then be defined thus:
`
injective family F a :: *
type instance F Int = Bool
type instance F Bool = Int
injective family G a :: *
type instance G a = a
`
Syntax is of course completely changeable; I've simply picked one of the possible designs. Hopefully this won't be subjected to too much bike-shedding.
- Add the constructor `InjFamilyTyCon` to `TyConRhs` and the family flavour `InjectiveFamily` to `HsSyn`. Again, I've opted to encode injectivity as a flavour rather than (say) a `Bool` attached to type families. This is a completely arbitrary choice and may be utterly stupid.
- Altered the definition of decomposable `TyCon`s to include injective families (`isDecomposableTyCon`). This effectively introduces a typing rule that says if we have `(F a ~ F b)` then we can deduce `(a ~ b)` (`TcCanonical`).
- Modified the unifier so that it will attempt to replace saturated injective families with their left-hand sides where possible (`TcUnify`). This means that in a function such as:
`
f :: F a -> F a
f = ...
`
The type of `f False` is inferred as `F Int` (i.e., `a` is no longer ambiguous).
Some things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate `f False` I get nothing (not even a Segmentation fault).
See what you think.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | --------------------- |
| Version | 7.4.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj@microsoft.com |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Injective type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj@microsoft.com"],"type":"FeatureRequest","description":"Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.\r\n\r\nI've naively attempted a proof-of-concept in GHC. It's almost certainly incorrect and probably breaks the type system, but I thought it best to put it here and see if it can be made workable.\r\n\r\nIn summary, my changes are:\r\n\r\n * Add a new keyword, {{{injective}}}, which is available only when the {{{TypeFamilies}}} extension is enabled. Injective families may then be defined thus:\r\n\r\n {{{\r\n injective family F a :: *\r\n type instance F Int = Bool\r\n type instance F Bool = Int\r\n\r\n injective family G a :: *\r\n type instance G a = a\r\n }}}\r\n\r\n Syntax is of course completely changeable; I've simply picked one of the possible designs. Hopefully this won't be subjected to too much bike-shedding.\r\n\r\n * Add the constructor {{{InjFamilyTyCon}}} to {{{TyConRhs}}} and the family flavour {{{InjectiveFamily}}} to {{{HsSyn}}}. Again, I've opted to encode injectivity as a flavour rather than (say) a {{{Bool}}} attached to type families. This is a completely arbitrary choice and may be utterly stupid.\r\n\r\n * Altered the definition of decomposable {{{TyCon}}}s to include injective families ({{{isDecomposableTyCon}}}). This effectively introduces a typing rule that says if we have {{{(F a ~ F b)}}} then we can deduce {{{(a ~ b)}}} ({{{TcCanonical}}}).\r\n\r\n * Modified the unifier so that it will attempt to replace saturated injective families with their left-hand sides where possible ({{{TcUnify}}}). This means that in a function such as:\r\n\r\n {{{\r\n f :: F a -> F a\r\n f = ...\r\n }}}\r\n\r\n The type of {{{f False}}} is inferred as {{{F Int}}} (i.e., {{{a}}} is no longer ambiguous).\r\n\r\nSome things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate {{{f False}}} I get nothing (not even a Segmentation fault).\r\n\r\nSee what you think.\r\n ","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/4259Relax restrictions on type family instance overlap2019-07-07T18:59:48ZlilacRelax restrictions on type family instance overlapThe following reduced fragment of some real code is rejected, but could be accepted, by GHC:
```
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (...The following reduced fragment of some real code is rejected, but could be accepted, by GHC:
```
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (f a) (f b) = LessEq a b
```
GHC says:
```
Conflicting family instance declarations:
type instance LessEq a a
-- Defined at /home/richards/.random/tf.hs:5:14-19
type instance LessEq (f a) (f b)
-- Defined at /home/richards/.random/tf.hs:6:14-19
```
This is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of -XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.
In particular (absent -XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.
In order to retain soundness in the presence of -XUndecidableInstances, any pair of type instances, where either instance could not be compiled without -XUndecidableInstances, would continue to use the current syntactic equality rule.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.12.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family instance conflict checks could be smarter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The following reduced fragment of some real code is rejected, but could be accepted, by GHC:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}\r\ndata True\r\n\r\ntype family LessEq a b :: *\r\ntype instance LessEq a a = True\r\ntype instance LessEq (f a) (f b) = LessEq a b\r\n}}}\r\n\r\nGHC says:\r\n\r\n{{{\r\n Conflicting family instance declarations:\r\n type instance LessEq a a\r\n -- Defined at /home/richards/.random/tf.hs:5:14-19\r\n type instance LessEq (f a) (f b)\r\n -- Defined at /home/richards/.random/tf.hs:6:14-19\r\n}}}\r\n\r\nThis is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of -XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.\r\n\r\nIn particular (absent -XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.\r\n\r\nIn order to retain soundness in the presence of -XUndecidableInstances, any pair of type instances, where either instance could not be compiled without -XUndecidableInstances, would continue to use the current syntactic equality rule.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1