GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:29:39Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11599Why is UndecidableInstances required for an obviously terminating type family?2019-07-07T18:29:39ZGabor GreifWhy is UndecidableInstances required for an obviously terminating type family?In below (working) snippet
```hs
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances #-}
type family Rev (acc :: [*]) (ts :: [*]) :: [*] where
Rev acc '[] = acc
Rev acc (t ': ts) = Rev (t ': acc) ts
type Rev...In below (working) snippet
```hs
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances #-}
type family Rev (acc :: [*]) (ts :: [*]) :: [*] where
Rev acc '[] = acc
Rev acc (t ': ts) = Rev (t ': acc) ts
type Reverse ts = Rev '[] ts
```
the `Rev` does an exhaustive pattern match on its second argument and recurses on strictly smaller data.
```hs
*Main> :kind! Reverse [Char, Bool, Float]
Reverse [Char, Bool, Float] :: [*]
= '[Float, Bool, Char]
```
So when I remove `UndecidableInstances` it is not clear to me why this would be rejected :-(
```
error:
The type family application Rev (a : acc) as
is no smaller than the instance head
(Use UndecidableInstances to permit this)
In the equations for closed type family Rev
In the type family declaration for Rev
Failed, modules loaded: none.
```
I tried this on GHC v8.1.today, but older GHCs behave the same.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"Why is UndecidableInstances required for an obviously terminating type family?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In below (working) snippet\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances #-}\r\n\r\ntype family Rev (acc :: [*]) (ts :: [*]) :: [*] where\r\n Rev acc '[] = acc\r\n Rev acc (t ': ts) = Rev (t ': acc) ts\r\n\r\ntype Reverse ts = Rev '[] ts\r\n}}}\r\nthe `Rev` does an exhaustive pattern match on its second argument and recurses on strictly smaller data.\r\n{{{#!hs\r\n*Main> :kind! Reverse [Char, Bool, Float]\r\nReverse [Char, Bool, Float] :: [*]\r\n= '[Float, Bool, Char]\r\n}}}\r\nSo when I remove `UndecidableInstances` it is not clear to me why this would be rejected :-(\r\n{{{\r\nerror:\r\n The type family application Rev (a : acc) as \r\n is no smaller than the instance head\r\n (Use UndecidableInstances to permit this)\r\n In the equations for closed type family Rev \r\n In the type family declaration for Rev \r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nI tried this on GHC v8.1.today, but older GHCs behave the same.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11594closed empty type families fully applied get reduced lazily when in a constr...2020-01-23T19:37:34ZCarter Schonwaldclosed empty type families fully applied get reduced lazily when in a constraint tuple and fully appliedin an effort to simulate the TypeError close type family in userland, I was doing a bit of experimentation with type families in ghc 7.10 and 8.0 RC2, and i was surprised to find that i can't get fully applied closed type families to red...in an effort to simulate the TypeError close type family in userland, I was doing a bit of experimentation with type families in ghc 7.10 and 8.0 RC2, and i was surprised to find that i can't get fully applied closed type families to reduce "strictly" when they are fully applied to concrete arguments within a Constraint Tuple.
Roughly, I want to be able to write "Assert x" style predicates in a type signature, and have those be checked/ reduced at the definition site rather than the use site. It seems like what I would have to do is do a slight indirection the form
```
publicFunName :: SimpleType c1 c2 --- c1 c2 are two concrete types
publicFunName ... = guardedFun
where
guardedFun :: (MyClosedTypeFamAssert c1 c2)=> SimpleType c1 c2
guardedFun ... = ...
-- myClosedTypeFamAssert (x :: *) (y :: *) :: Constraint
```
I guess this SORTOF makes sense that it doesn't get reduced strictly at the definition site (though its a sort of normalization i feel like). I think the sibling computation where i have `myClosedTypeFamAssert (x :: *) (y :: *) :: Bool` and have the guard be ('True \~ myClosedTypeFamAssert c1 c2 ), but I was hoping i could have things look a teeny bit more "Assertion" style for aesthetical reasons
enclosed below is a self contained module that exhibits a more worked out example
```
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs #-}
{-# LANGUAGE TypeInType, ConstraintKinds #-}
module Main where
import GHC.Types (Constraint,TYPE,Levity(..))
main = print (7 :: Int)-- this works
-- main = print (sevenBad :: Int ) -- this does error, but its at the use site rather than definition site!
-- using this one ""works"", but results in a VERY confusing type error involving
--
type family WorstClosedStuckError (x :: a) :: Constraint where
WorstClosedStuckError a = (False ~ True)
--- empty closed type families are ONLY allowed as of ghc 8.0
type family ClosedStuckSilly (x :: a) :: b where
type family ClosedStuckSillyConstr (x :: a) :: Constraint where
--- this is analogous to a version of the TypeError family in GHC.TypeLits in 8.0 onwards
--- but kind polymorphic closed empty type families dont seem to trigger a type error in the definition site
--- but rather in the USE site
type family ClosedStuckTypeConstr (x :: TYPE Lifted) :: Constraint where
type family ClosedStuckType (x :: TYPE Lifted) :: b where
--- these two seem to work OK
-- these two only only report an error once I resolve the constraint on a to something like Int etc
sevenBad :: (ClosedStuckSilly 'True , Num a) => a
sevenBad = 7
sevenOtherBad :: (ClosedStuckSillyConstr 'False, Num a) => a
sevenOtherBad = 7
-- this one fails to type check at the definition site, but has a SUPER confusing
-- error about allow ambiguous types
sevenBadWorst :: (WorstClosedStuckError 'False, Num a) => a
sevenBadWorst = 7
sevenOKButNotUseful :: (ClosedStuckType Bool, Num a) => a
sevenOKButNotUseful = 7
-- i have to do an indirection to force an "assertion" / "reduction", the following triggers the error as expected
sevenIndirect :: Num a => a
sevenIndirect = sevenBad
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | Bug |
| 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":"closed empty type families fully applied get reduced lazily when in a constraint tuple and fully applied","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"in an effort to simulate the TypeError close type family in userland, I was doing a bit of experimentation with type families in ghc 7.10 and 8.0 RC2, and i was surprised to find that i can't get fully applied closed type families to reduce \"strictly\" when they are fully applied to concrete arguments within a Constraint Tuple.\r\n\r\nRoughly, I want to be able to write \"Assert x\" style predicates in a type signature, and have those be checked/ reduced at the definition site rather than the use site. It seems like what I would have to do is do a slight indirection the form \r\n\r\n{{{\r\npublicFunName :: SimpleType c1 c2 --- c1 c2 are two concrete types \r\npublicFunName ... = guardedFun\r\n where \r\n guardedFun :: (MyClosedTypeFamAssert c1 c2)=> SimpleType c1 c2\r\n guardedFun ... = ... \r\n -- myClosedTypeFamAssert (x :: *) (y :: *) :: Constraint \r\n}}}\r\n\r\nI guess this SORTOF makes sense that it doesn't get reduced strictly at the definition site (though its a sort of normalization i feel like). I think the sibling computation where i have `myClosedTypeFamAssert (x :: *) (y :: *) :: Bool` and have the guard be ('True ~ myClosedTypeFamAssert c1 c2 ), but I was hoping i could have things look a teeny bit more \"Assertion\" style for aesthetical reasons\r\n\r\nenclosed below is a self contained module that exhibits a more worked out example \r\n\r\n{{{\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE FlexibleInstances #-} \r\n\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies, TypeOperators #-}\r\n{-# LANGUAGE DataKinds, GADTs #-}\r\n{-# LANGUAGE TypeInType, ConstraintKinds #-}\r\n\r\nmodule Main where\r\n\r\nimport GHC.Types (Constraint,TYPE,Levity(..))\r\n\r\nmain = print (7 :: Int)-- this works\r\n-- main = print (sevenBad :: Int ) -- this does error, but its at the use site rather than definition site!\r\n\r\n\r\n-- using this one \"\"works\"\", but results in a VERY confusing type error involving \r\n-- \r\ntype family WorstClosedStuckError (x :: a) :: Constraint where \r\n WorstClosedStuckError a = (False ~ True)\r\n\r\n\r\n--- empty closed type families are ONLY allowed as of ghc 8.0\r\ntype family ClosedStuckSilly (x :: a) :: b where \r\ntype family ClosedStuckSillyConstr (x :: a) :: Constraint where \r\n--- this is analogous to a version of the TypeError family in GHC.TypeLits in 8.0 onwards\r\n--- but kind polymorphic closed empty type families dont seem to trigger a type error in the definition site \r\n--- but rather in the USE site \r\n\r\ntype family ClosedStuckTypeConstr (x :: TYPE Lifted) :: Constraint where \r\ntype family ClosedStuckType (x :: TYPE Lifted) :: b where \r\n --- these two seem to work OK \r\n\r\n-- these two only only report an error once I resolve the constraint on a to something like Int etc\r\nsevenBad :: (ClosedStuckSilly 'True , Num a) => a \r\nsevenBad = 7 \r\nsevenOtherBad :: (ClosedStuckSillyConstr 'False, Num a) => a \r\nsevenOtherBad = 7 \r\n\r\n-- this one fails to type check at the definition site, but has a SUPER confusing \r\n-- error about allow ambiguous types\r\nsevenBadWorst :: (WorstClosedStuckError 'False, Num a) => a\r\nsevenBadWorst = 7 \r\n\r\nsevenOKButNotUseful :: (ClosedStuckType Bool, Num a) => a \r\nsevenOKButNotUseful = 7 \r\n\r\n-- i have to do an indirection to force an \"assertion\" / \"reduction\", the following triggers the error as expected\r\nsevenIndirect :: Num a => a\r\nsevenIndirect = sevenBad\r\n\r\n\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11581TypeError requires UndecidableInstances unnecessarily2021-08-03T22:02:50ZrwbartonTypeError requires UndecidableInstances unnecessarilyThe example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
...The example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
```
requires `UndecidableInstances`:
```
BS.hs:11:5: error:
• The type family application ‘(TypeError ...)’
is no smaller than the instance head
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘ByteSize’
In the type family declaration for ‘ByteSize’
```
Obviously there's no real danger of undecidability here.
I tried changing the declaration of `TypeError` to
```hs
type family TypeError :: ErrorMessage -> b where
```
but it didn't help. Same error. Is that a bug?https://gitlab.haskell.org/ghc/ghc/-/issues/11534Allow class associated types to reference functional dependencies2021-01-02T05:27:44ZEdward KmettAllow class associated types to reference functional dependenciesConsider:
```hs
class Foo i j | i -> j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by t...Consider:
```hs
class Foo i j | i -> j where
type Bar i :: *
type Bar i = j
```
This is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the \| i -\> j functional dependency on the class.
This would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| 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":"Allow class associated types to reference functional dependencies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["FunctionalDependencies","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider:\r\n\r\n{{{#!hs\r\nclass Foo i j | i -> j where\r\n type Bar i :: *\r\n type Bar i = j\r\n}}}\r\n\r\nThis is rejected as `j` is not an argument to `Bar`, but when we realize any instance `j` will be a known type, determined by `i`, as told to us by the | i -> j functional dependency on the class.\r\n\r\nThis would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11523Infinite Loop when mixing UndecidableSuperClasses and the class/instance cons...2019-07-07T18:30:04ZEdward KmettInfinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.There seems to be a bad interaction between `UndecidableSuperClasses` and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level:
```hs
class (Foo f, Bar f) => Baz f
instance (Foo ...There seems to be a bad interaction between `UndecidableSuperClasses` and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level:
```hs
class (Foo f, Bar f) => Baz f
instance (Foo f, Bar f) => Baz f
```
Unfortunately, there are circumstances in which you can't eliminate it, such as
```hs
class (p, q) => p & q
instance (p, q) => p & q
```
There we can't partially apply (,) at the constraint level, but we can talk about `(&) :: Constraint -> Constraint -> Constraint` and `(&) (Eq a) :: Constraint -> Constraint`.
This doesn't seem to happen on simpler examples like the above, but once I modify the categories example from #11480 to move the domain and codomain of a functor into class associated types, so that they don't infect every single subclass of functor, we run into a problem. The following stripped down version of the code seems to send the compiler into an infinite loop:
```hs
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}
{-# language FlexibleInstances #-}
{-# language TypeOperators #-}
{-# language ScopedTypeVariables #-}
{-# language DefaultSignatures #-}
{-# language FunctionalDependencies #-}
{-# language UndecidableSuperClasses #-}
{-# language UndecidableInstances #-}
{-# language TypeInType #-}
import GHC.Types (Constraint, Type)
import qualified Prelude
type Cat i = i -> i -> Type
newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
class Vacuous (a :: i)
instance Vacuous a
class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where
type Op p :: Cat i
type Op p = Y p
type Ob p :: i -> Constraint
type Ob p = Vacuous
class (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where
type Dom f :: Cat i
type Cod f :: Cat j
class (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q
instance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)
data Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)
instance (Category p, Category q) => Category (Nat p q) where
type Ob (Nat p q) = Fun p q
instance (Category p, Category q) => Functor (Nat p q) where
type Dom (Nat p q) = Y (Nat p q)
type Cod (Nat p q) = Nat (Nat p q) (->)
instance (Category p, Category q) => Functor (Nat p q f) where
type Dom (Nat p q f) = Nat p q
type Cod (Nat p q f) = (->)
instance Category (->)
instance Functor ((->) e) where
type Dom ((->) e) = (->)
type Cod ((->) e) = (->)
instance Functor (->) where
type Dom (->) = Y (->)
type Cod (->) = Nat (->) (->)
instance (Category p, Op p ~ Y p) => Category (Y p) where
type Op (Y p) = p
instance (Category p, Op p ~ Y p) => Functor (Y p a) where
type Dom (Y p a) = Y p
type Cod (Y p a) = (->)
instance (Category p, Op p ~ Y p) => Functor (Y p) where
type Dom (Y p) = p
type Cod (Y p) = Nat (Y p) (->)
```
Here I need the circular definition of `Fun` to talk about the fact that the objects in the category of natural transformations from a category p to a category q are functors with domain p and codomain q, so to give the definition of the class-associated `type Ob (Nat p q)` I need such a cyclic definition.
I can't leave the domain and codomain of `Functor` in fundeps, otherwise if I go to define a subclass of Functor I'd have to include the arguments, and I have a *lot* of those subclasses!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Infinite Loop when mixing UndecidableSuperClasses and the class/instance constraint synonym trick.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"There seems to be a bad interaction between `UndecidableSuperClasses` and the common trick of using a cyclic definition of a class and instance to make an alias at the constraint level:\r\n\r\n{{{#!hs\r\nclass (Foo f, Bar f) => Baz f\r\ninstance (Foo f, Bar f) => Baz f\r\n}}}\r\n\r\nUnfortunately, there are circumstances in which you can't eliminate it, such as\r\n\r\n{{{#!hs\r\nclass (p, q) => p & q\r\ninstance (p, q) => p & q\r\n}}}\r\n\r\nThere we can't partially apply (,) at the constraint level, but we can talk about `(&) :: Constraint -> Constraint -> Constraint` and `(&) (Eq a) :: Constraint -> Constraint`.\r\n\r\nThis doesn't seem to happen on simpler examples like the above, but once I modify the categories example from #11480 to move the domain and codomain of a functor into class associated types, so that they don't infect every single subclass of functor, we run into a problem. The following stripped down version of the code seems to send the compiler into an infinite loop:\r\n\r\n{{{#!hs\r\n{-# language KindSignatures #-}\r\n{-# language PolyKinds #-}\r\n{-# language DataKinds #-}\r\n{-# language TypeFamilies #-}\r\n{-# language RankNTypes #-}\r\n{-# language NoImplicitPrelude #-}\r\n{-# language FlexibleContexts #-}\r\n{-# language MultiParamTypeClasses #-}\r\n{-# language GADTs #-}\r\n{-# language ConstraintKinds #-}\r\n{-# language FlexibleInstances #-}\r\n{-# language TypeOperators #-}\r\n{-# language ScopedTypeVariables #-}\r\n{-# language DefaultSignatures #-}\r\n{-# language FunctionalDependencies #-}\r\n{-# language UndecidableSuperClasses #-}\r\n{-# language UndecidableInstances #-}\r\n{-# language TypeInType #-}\r\n\r\nimport GHC.Types (Constraint, Type)\r\nimport qualified Prelude\r\n\r\ntype Cat i = i -> i -> Type\r\n\r\nnewtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }\r\n\r\nclass Vacuous (a :: i)\r\ninstance Vacuous a\r\n\r\nclass (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->)) => Category (p :: Cat i) where\r\n type Op p :: Cat i\r\n type Op p = Y p\r\n type Ob p :: i -> Constraint\r\n type Ob p = Vacuous\r\n\r\nclass (Category (Dom f), Category (Cod f)) => Functor (f :: i -> j) where\r\n type Dom f :: Cat i\r\n type Cod f :: Cat j\r\n\r\nclass (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j) | f -> p q\r\ninstance (Functor f, Dom f ~ p, Cod f ~ q) => Fun (p :: Cat i) (q :: Cat j) (f :: i -> j)\r\n\r\ndata Nat (p :: Cat i) (q :: Cat j) (f :: i -> j) (g :: i -> j)\r\n\r\ninstance (Category p, Category q) => Category (Nat p q) where\r\n type Ob (Nat p q) = Fun p q\r\n\r\ninstance (Category p, Category q) => Functor (Nat p q) where\r\n type Dom (Nat p q) = Y (Nat p q)\r\n type Cod (Nat p q) = Nat (Nat p q) (->)\r\n\r\ninstance (Category p, Category q) => Functor (Nat p q f) where\r\n type Dom (Nat p q f) = Nat p q\r\n type Cod (Nat p q f) = (->)\r\n\r\ninstance Category (->) \r\n\r\ninstance Functor ((->) e) where\r\n type Dom ((->) e) = (->)\r\n type Cod ((->) e) = (->)\r\n\r\ninstance Functor (->) where\r\n type Dom (->) = Y (->)\r\n type Cod (->) = Nat (->) (->)\r\n\r\ninstance (Category p, Op p ~ Y p) => Category (Y p) where\r\n type Op (Y p) = p\r\n\r\ninstance (Category p, Op p ~ Y p) => Functor (Y p a) where\r\n type Dom (Y p a) = Y p\r\n type Cod (Y p a) = (->)\r\n\r\ninstance (Category p, Op p ~ Y p) => Functor (Y p) where\r\n type Dom (Y p) = p\r\n type Cod (Y p) = Nat (Y p) (->)\r\n}}}\r\n\r\nHere I need the circular definition of `Fun` to talk about the fact that the objects in the category of natural transformations from a category p to a category q are functors with domain p and codomain q, so to give the definition of the class-associated `type Ob (Nat p q)` I need such a cyclic definition.\r\n\r\nI can't leave the domain and codomain of `Functor` in fundeps, otherwise if I go to define a subclass of Functor I'd have to include the arguments, and I have a ''lot'' of those subclasses!","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11511Type family producing infinite type accepted as injective2019-07-07T18:30:07ZJan Stolarekjan.stolarek@ed.ac.ukType family producing infinite type accepted as injectiveA question came up during discussion at University of Wrocław:
```hs
type family F a = r | r -> a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool`...A question came up during discussion at University of Wrocław:
```hs
type family F a = r | r -> a where
F a = [F a]
```
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.
This is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family producing infinite type accepted as injective","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"Bug","description":"A question came up during discussion at University of Wrocław:\r\n\r\n\r\n{{{#!hs\r\ntype family F a = r | r -> a where\r\n F a = [F a]\r\n}}}\r\n\r\nShould this pass the injectivity check? Currently it does but I don't think this is correct. After all `F Bool` and `F Char` both reduce to the same infinite type `[[[...]]]`, which by definition of injectivity gives us `Char ~ Bool`. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.\r\n\r\nThis is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11424"Occurs check" not considered when reducing closed type families2019-07-07T18:30:28ZIavor S. Diatchki"Occurs check" not considered when reducing closed type familiesHello,
consider the following example:
```hs
{-# LANGUAGE TypeFamilies #-}
type family Same a b where
Same a a = Int
Same a b = Char
example :: Same a [a] -> a
example = undefined
bad :: a
bad = example 'c'
```
This program sho...Hello,
consider the following example:
```hs
{-# LANGUAGE TypeFamilies #-}
type family Same a b where
Same a a = Int
Same a b = Char
example :: Same a [a] -> a
example = undefined
bad :: a
bad = example 'c'
```
This program should type check, using the following reasoning: `a` and `[a]` can never be equal, therefore the first equation for `Same` does not apply, and so we can fall trough to the second one, thus reducing `Same` to `Char`. Therefore, `bad` should be accept.
GHC rejects this program with the following error:
```
• Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’
• In the first argument of ‘example’, namely ‘'c'’
In the expression: example 'c'
In an equation for ‘bad’: bad = example 'c'
• Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| 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":"\"Occurs check\" not considered when reducing closed type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Hello,\r\n\r\nconsider the following example:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family Same a b where\r\n Same a a = Int\r\n Same a b = Char\r\n\r\nexample :: Same a [a] -> a\r\nexample = undefined\r\n\r\nbad :: a\r\nbad = example 'c'\r\n}}}\r\n\r\nThis program should type check, using the following reasoning: `a` and `[a]` can never be equal, therefore the first equation for `Same` does not apply, and so we can fall trough to the second one, thus reducing `Same` to `Char`. Therefore, `bad` should be accept.\r\n\r\nGHC rejects this program with the following error:\r\n{{{\r\n • Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’\r\n • In the first argument of ‘example’, namely ‘'c'’\r\n In the expression: example 'c'\r\n In an equation for ‘bad’: bad = example 'c'\r\n • Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11384Error says to fix incorrect return type2020-01-23T19:37:34ZIcelandjackError says to fix incorrect return typeDefining a constructor that returns the wrong type (non-parent type).
If the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:
```
Prelude> data A
Prelu...Defining a constructor that returns the wrong type (non-parent type).
If the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:
```
Prelude> data A
Prelude> data B a where MkB :: A ()
<interactive>:2:23: error:
• Expecting one fewer argument to ‘A’
Expected kind ‘* -> *’, but ‘A’ has kind ‘*’
• In the type ‘A ()’
In the definition of data constructor ‘MkB’
In the data declaration for ‘B’
```
Expected:
1. Suggest GADTs:
```
• Illegal generalised algebraic data declaration for ‘B’
(Use GADTs to allow GADTs)
• In the data declaration for ‘B’
```
1. Complain about incorrect return type:
```
• Data constructor ‘MkB’ returns type ‘A’
instead of an instance of its parent type ‘B a’
• In the definition of data constructor ‘MkB’
In the data type declaration for ‘B’
```
It shouldn't suggest the user fix the incorrect return type
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Error says to fix incorrect return type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Defining a constructor that returns the wrong type (non-parent type).\r\n\r\nIf the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:\r\n\r\n{{{\r\nPrelude> data A\r\nPrelude> data B a where MkB :: A ()\r\n\r\n<interactive>:2:23: error:\r\n • Expecting one fewer argument to ‘A’\r\n Expected kind ‘* -> *’, but ‘A’ has kind ‘*’\r\n • In the type ‘A ()’\r\n In the definition of data constructor ‘MkB’\r\n In the data declaration for ‘B’\r\n}}}\r\n\r\nExpected:\r\n1. Suggest GADTs:\r\n{{{\r\n• Illegal generalised algebraic data declaration for ‘B’\r\n (Use GADTs to allow GADTs)\r\n• In the data declaration for ‘B’\r\n}}}\r\n2. Complain about incorrect return type:\r\n{{{\r\n• Data constructor ‘MkB’ returns type ‘A’ \r\n instead of an instance of its parent type ‘B a’\r\n• In the definition of data constructor ‘MkB’\r\n In the data type declaration for ‘B’\r\n}}}\r\n\r\nIt shouldn't suggest the user fix the incorrect return type","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11369Suppress redundant-constraint warnings in case of empty classes2020-01-23T19:37:34ZHerbert Valerio Riedelhvr@gnu.orgSuppress redundant-constraint warnings in case of empty classesThe technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
r...The technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
readFoo :: Throws IOError => FilePath -> IO Foo
readFoo fn = {- ... -}
```
which GHC 8.0 warns about.
I propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, edsko |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress redundant-constraint warnings in case of empty classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","edsko"],"type":"Bug","description":"The technique described in\r\n\r\nhttp://www.well-typed.com/blog/2015/07/checked-exceptions/\r\n\r\nmakes use of a class without any methods, i.e.\r\n\r\n{{{#!hs\r\nclass Throws e\r\n}}}\r\n\r\nHowever, this by definition results in redundant constraints, e.g.\r\n\r\n{{{#!hs\r\nreadFoo :: Throws IOError => FilePath -> IO Foo\r\nreadFoo fn = {- ... -}\r\n}}}\r\n\r\nwhich GHC 8.0 warns about.\r\n\r\nI propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.","type_of_failure":"OtherFailure","blocking":[]} -->Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11352Allow applying type to label2023-06-05T11:55:16ZIcelandjackAllow applying type to label```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #...```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
import GHC.OverloadedLabels
instance IsLabel "answer" Int where
fromLabel _ = 42
answer :: IsLabel "answer" a => a
answer = #answer
```
The follow works:
```hs
>>> answer @Int
42
```
but fails with a label:
```hs
>>> #answer @Int
<interactive>:...:1: error:
• Cannot not apply expression of type ‘t0’
to a visible type argument ‘Int’
• In the expression: #answer @Int
In an equation for ‘it’: it = #answer @Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Allow applying type to label","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE OverloadedLabels #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE DataKinds #-}\r\n\r\nimport GHC.TypeLits\r\nimport GHC.OverloadedLabels\r\n\r\ninstance IsLabel \"answer\" Int where\r\n fromLabel _ = 42\r\n\r\nanswer :: IsLabel \"answer\" a => a\r\nanswer = #answer\r\n}}}\r\n\r\nThe follow works:\r\n\r\n{{{#!hs\r\n>>> answer @Int\r\n42\r\n}}}\r\n\r\nbut fails with a label:\r\n\r\n{{{#!hs\r\n>>> #answer @Int\r\n<interactive>:...:1: error:\r\n • Cannot not apply expression of type ‘t0’\r\n to a visible type argument ‘Int’\r\n • In the expression: #answer @Int\r\n In an equation for ‘it’: it = #answer @Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->isovectorisovectorhttps://gitlab.haskell.org/ghc/ghc/-/issues/11186Give strong preference to type variable names in scope when reporting hole co...2019-07-07T18:31:35ZDavid FeuerGive strong preference to type variable names in scope when reporting hole contextsWhen using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recentl...When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like
```hs
foo :: forall bar . ...
foo = ... _ ...
```
and yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| 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":"Give strong preference to type variable names in scope when reporting hole contexts","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":["typed-holes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like\r\n\r\n{{{#!hs\r\nfoo :: forall bar . ...\r\nfoo = ... _ ...\r\n}}}\r\n\r\nand yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11169Remove the word "skolem" from user error messages2019-07-07T18:31:39ZDavid FeuerRemove the word "skolem" from user error messagesSkolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages sho...Skolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages should explain things at the Haskell level.
```
Couldn't match expected type ‘t’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by...
```
I'd much rather see an explanation using words like "existentially quantified" and "right-hand side of a pattern match".
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| 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":"Remove the word \"skolem\" from user error messages","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Skolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages should explain things at the Haskell level.\r\n\r\n{{{\r\n Couldn't match expected type ‘t’ with actual type ‘a’\r\n because type variable ‘a’ would escape its scope\r\n This (rigid, skolem) type variable is bound by...\r\n}}}\r\n\r\nI'd much rather see an explanation using words like \"existentially quantified\" and \"right-hand side of a pattern match\".","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11141Better error message when instance signature is incorrect2019-07-07T18:31:47ZEdward Z. YangBetter error message when instance signature is incorrectI was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):
```
{-# LANGUAGE FunctionalDependencie...I was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):
```
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module A where
data F a = F a
instance Show a => Show (F a) where
show :: forall a. Show a => F a -> String
show (F x) = show x
```
This instance signature is incorrect: it's not necessary to add a universal quantifier to scope over type variables defined in the instance head; they are automatically in scope. But GHC unhelpfully reports:
```
ezyang@sabre:~$ Dev/ghc-7.10.2/usr/bin/ghci A.hs
GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling A ( A.hs, interpreted )
A.hs:8:13:
Could not deduce (Show a0)
from the context (Show a)
bound by the type signature for show :: Show a => F a -> String
at A.hs:8:13-45
The type variable ‘a0’ is ambiguous
When checking that:
forall a. Show a => forall a1. Show a1 => F a1 -> String
is more polymorphic than: forall a. Show a => F a -> String
When checking that instance signature for ‘show’
is more general than its signature in the class
Instance sig: forall a.
Show a =>
forall a1. Show a1 => F a1 -> String
Class sig: forall a. Show a => F a -> String
In the instance declaration for ‘Show (F a)’
Failed, modules loaded: none.
```
Why did I get the wrong idea about how instance signatures work? Well, GHC doesn't warn if you write this:
```
instance Show a => Show (F a) where
show :: Show a => F a -> String
show (F x) = show x
```
Because this turns into a full type signature 'Show a, Show a =\> F a -\> String' (the first a and the second a end up getting unified.) I'm not sure if it should warn; it's an easy mistake to make if you are treating instance methods like plain function definitions (of course you have to write the full type signature...)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | Bug |
| 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":"Better error message when instance signature is incorrect","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):\r\n\r\n{{{\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE InstanceSigs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\nmodule A where\r\n\r\ndata F a = F a\r\ninstance Show a => Show (F a) where\r\n show :: forall a. Show a => F a -> String\r\n show (F x) = show x\r\n}}}\r\n\r\nThis instance signature is incorrect: it's not necessary to add a universal quantifier to scope over type variables defined in the instance head; they are automatically in scope. But GHC unhelpfully reports:\r\n\r\n{{{\r\nezyang@sabre:~$ Dev/ghc-7.10.2/usr/bin/ghci A.hs\r\nGHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling A ( A.hs, interpreted )\r\n\r\nA.hs:8:13:\r\n Could not deduce (Show a0)\r\n from the context (Show a)\r\n bound by the type signature for show :: Show a => F a -> String\r\n at A.hs:8:13-45\r\n The type variable ‘a0’ is ambiguous\r\n When checking that:\r\n forall a. Show a => forall a1. Show a1 => F a1 -> String\r\n is more polymorphic than: forall a. Show a => F a -> String\r\n When checking that instance signature for ‘show’\r\n is more general than its signature in the class\r\n Instance sig: forall a.\r\n Show a =>\r\n forall a1. Show a1 => F a1 -> String\r\n Class sig: forall a. Show a => F a -> String\r\n In the instance declaration for ‘Show (F a)’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nWhy did I get the wrong idea about how instance signatures work? Well, GHC doesn't warn if you write this:\r\n\r\n{{{\r\ninstance Show a => Show (F a) where\r\n show :: Show a => F a -> String\r\n show (F x) = show x\r\n}}}\r\n\r\nBecause this turns into a full type signature 'Show a, Show a => F a -> String' (the first a and the second a end up getting unified.) I'm not sure if it should warn; it's an easy mistake to make if you are treating instance methods like plain function definitions (of course you have to write the full type signature...)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11115Indicate missing associated type instances2019-07-07T18:31:53ZrimmingtonIndicate missing associated type instancesIf there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:
```
...If there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:
```
<interactive>:98:20:
Couldn't match type ‘units-2.3:Data.Metrology.Factor.Normalize
(Data.Metrology.Suspicious.Poly.SurfaceUnitFactorsOf
(Data.Singletons.Prelude.Tuple.Snd
(Data.Metrology.Suspicious.Poly.SplitPrefix
(PrefixExp Deci) Deci Core))
units-2.3:Data.Metrology.Factor.@- '['units-2.3:Data.Metrology.Factor.F
Core
('Data.Metrology.Z.S
'Data.Metrology.Z.Zero)])’
with ‘'[]’
In the expression: (25 %> centi Core) `ceilToUnit` deci Core
In an equation for ‘it’:
it = (25 %> centi Core) `ceilToUnit` deci Core
```
The cause of the above error message is that `Deci` is not a member of the typeclass `ExpUnitPrefix` that defines the associated type `PrefixExp`. Unfortunately this is not clear at all from the error message, and adding additional class constraints to the appropriate functions doesn't improve things.
It would be nice if GHC pointed out that there is no `ExpUnitPrefix Deci` instance, or at least that `PrefixExp Deci` cannot be further reduced. I imagine this would be useful for open type families as well, but I can't comment personally.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| 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":"Indicate missing associated type instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"If there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:\r\n\r\n{{{\r\n<interactive>:98:20:\r\n Couldn't match type ‘units-2.3:Data.Metrology.Factor.Normalize\r\n (Data.Metrology.Suspicious.Poly.SurfaceUnitFactorsOf\r\n (Data.Singletons.Prelude.Tuple.Snd\r\n (Data.Metrology.Suspicious.Poly.SplitPrefix\r\n (PrefixExp Deci) Deci Core))\r\n units-2.3:Data.Metrology.Factor.@- '['units-2.3:Data.Metrology.Factor.F\r\n Core\r\n ('Data.Metrology.Z.S\r\n 'Data.Metrology.Z.Zero)])’\r\n with ‘'[]’\r\n In the expression: (25 %> centi Core) `ceilToUnit` deci Core\r\n In an equation for ‘it’:\r\n it = (25 %> centi Core) `ceilToUnit` deci Core\r\n}}}\r\n\r\nThe cause of the above error message is that `Deci` is not a member of the typeclass `ExpUnitPrefix` that defines the associated type `PrefixExp`. Unfortunately this is not clear at all from the error message, and adding additional class constraints to the appropriate functions doesn't improve things.\r\n\r\nIt would be nice if GHC pointed out that there is no `ExpUnitPrefix Deci` instance, or at least that `PrefixExp Deci` cannot be further reduced. I imagine this would be useful for open type families as well, but I can't comment personally.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11099Incorrect warning about redundant constraints2019-07-07T18:32:07ZIavor S. DiatchkiIncorrect warning about redundant constraintsThe following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
...The following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
```
Redundant constraint: SomeFun i ~ [a]
In the type signature for:
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
```
I tried it on GHC version 7.11.20151029
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| 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":"Incorrect warning about redundant constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program results in an incorrect warning about a redundant constraint:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family SomeFun a \r\n\r\nf :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\nf _ = read \"HELLO\"\r\n}}}\r\n\r\nThis is the warning:\r\n{{{\r\nRedundant constraint: SomeFun i ~ [a]\r\n In the type signature for:\r\n f :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\n}}}\r\n\r\nI tried it on GHC version 7.11.20151029\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10978Anonymous type instances2019-07-07T18:32:49Zbenjamin.hodgsonAnonymous type instancesI find that commonly I write a `type family` (because it doesn't *need* to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.
Presently you're forced to u...I find that commonly I write a `type family` (because it doesn't *need* to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.
Presently you're forced to use type synonyms for all the instances of a `type family`, even if you don't intend to refer to the type by any name other than that of the type family. I find this tiresome:
```hs
type family F a
type instance F Char = Int
newtype FBool = FBool Int
type instance F Bool = FBool
data FInt = A | B | ...
type instance F Int = FInt
```
**I want to write `data instance`s and `newtype instance`s for `type` families**. These proposed constructs would introduce a new type without a name of its own (the only way to refer to it would be through the `type family`), just like the current design of `data` families. The above code would be roughly equivalent to:
```hs
type family F a
type instance F Char = Int -- already legal
newtype instance F Bool = FBool Int
data instance F Int = A | B | ...
```
I call this idea *anonymous type instances* but I'm open to suggestions for a snappier name.
Going the other way (writing a `type instance` for a `data family`) would remain illegal under this proposal.
```hs
data family G a
type instance G Char = Int -- still illegal
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| 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":"Anonymous type instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I find that commonly I write a `type family` (because it doesn't ''need'' to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.\r\n\r\nPresently you're forced to use type synonyms for all the instances of a `type family`, even if you don't intend to refer to the type by any name other than that of the type family. I find this tiresome:\r\n\r\n{{{#!hs\r\ntype family F a\r\n\r\ntype instance F Char = Int\r\n\r\nnewtype FBool = FBool Int\r\ntype instance F Bool = FBool\r\n\r\ndata FInt = A | B | ...\r\ntype instance F Int = FInt\r\n}}}\r\n\r\n'''I want to write `data instance`s and `newtype instance`s for `type` families'''. These proposed constructs would introduce a new type without a name of its own (the only way to refer to it would be through the `type family`), just like the current design of `data` families. The above code would be roughly equivalent to:\r\n\r\n{{{#!hs\r\ntype family F a\r\n\r\ntype instance F Char = Int -- already legal\r\nnewtype instance F Bool = FBool Int\r\ndata instance F Int = A | B | ...\r\n}}}\r\n\r\nI call this idea ''anonymous type instances'' but I'm open to suggestions for a snappier name.\r\n\r\n\r\nGoing the other way (writing a `type instance` for a `data family`) would remain illegal under this proposal.\r\n\r\n{{{#!hs\r\ndata family G a\r\n\r\ntype instance G Char = Int -- still illegal\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10833Use injective type families (decomposition) when dealing with givens2023-06-12T11:35:15ZJan Stolarekjan.stolarek@ed.ac.ukUse injective type families (decomposition) when dealing with givensConsider this code:
```hs
type family Id a = r | r -> a
id :: (Id a ~ Id b) => a -> b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints.
And yet ...Consider this code:
```hs
type family Id a = r | r -> a
id :: (Id a ~ Id b) => a -> b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints.
And yet `Coercion` has a form for representing such coercions, namely "nth" (written `SelCo` in GHC). We could say
```
co : F s1..sn ~ F t1..tn
F is injective in its i'th argument
-----------------------------------
SelCo (Tc i) co : si ~ ti
```
Indeed Lint already accepts such `SelCo`s:
```
lintCoercion the_co@(SelCo cs co)
= do { co' <- lintCoercion co
; let (Pair s t, co_role) = coercionKindRole co'
; if -- forall (both TyVar and CoVar)
...
-- TyCon
| Just (tc_s, tys_s) <- splitTyConApp_maybe s
, Just (tc_t, tys_t) <- splitTyConApp_maybe t
, tc_s == tc_t
, SelTyCon n r0 <- cs
, isInjectiveTyCon tc_s co_role
-- see Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
, tys_s `equalLength` tys_t
, tys_s `lengthExceeds` n
-> do { lintRole the_co (tyConRole co_role tc_s n) r0
; return (SelCo cs co') }
```
Note that `isInjectiveTyCon`! An injective type family is accepted here. (But only if it is injective in *all* arguments, which is stronger than we need.)
Allowing this would be user facing change, hence needing a GHC proposal. But it'd be very simple to implement.
@rae any views on how this might impact soundness?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #6018 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Use injective type families when dealing with givens","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[6018],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\ntype family Id a = r | r -> a\r\n\r\nid :: (Id a ~ Id b) => a -> b\r\nid x = x\r\n}}}\r\nGHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.","type_of_failure":"OtherFailure","blocking":[]} -->Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/10832Generalize injective type families2020-12-09T23:11:31ZJan Stolarekjan.stolarek@ed.ac.ukGeneralize injective type familiesWith injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a...With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a b r | a b -> r, r a -> b
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r)
```
Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:
```hs
type family AddTF a b = r | r a -> b where
AddTF Zero b = b
AddTF (Succ a) b = Succ (AddTF a b)
```
But we want to be able to say that.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| 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":"Generalize injective type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:\r\n\r\n{{{#!hs\r\ndata Nat = Zero | Succ a\r\n\r\nclass Add a b r | a b -> r, r a -> b\r\ninstance Add Zero b b\r\ninstance (Add a b r) => Add (Succ a) b (Succ r)\r\n}}}\r\nHere we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:\r\n\r\n{{{#!hs\r\ntype family AddTF a b = r | r a -> b where\r\n AddTF Zero b = b\r\n AddTF (Succ a) b = Succ (AddTF a b)\r\n}}}\r\nBut we want to be able to say that.","type_of_failure":"OtherFailure","blocking":[]} -->Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/10794Extension request: "where" clauses in type signatures2019-07-07T18:33:51ZdansoExtension request: "where" clauses in type signaturesSome type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow...Some type signatures could be simplified by separating certain elements, either because they are lengthy and can be expressed simpler, to better express intention, or because they are repetitive. A "WhereSignatures" extension would allow for type signatures like the following:
```hs
fold :: f -> [a] -> a
where f = a -> a -> a
-- expresses intention more clearly than:
fold :: (a -> a -> a) -> [a] -> a
union :: a -> a -> a
where a = Map.Map k v
-- much shorter/more readable than:
union :: Map.Map k v -> Map.Map k v -> Map.Map k v
```
Or maybe even:
```hs
fmap :: (a -> b) -> f a -> f b
where (Functor f)
-- arguably prettier than:
fmap :: (Functor f) => (a -> b) -> f a -> f b
```
This minor syntactic sugar is essentially equivalent to local "type" definitions, which provides an advantage of making the type's purpose more clear. This seems like a natural development on what the type checker can do.https://gitlab.haskell.org/ghc/ghc/-/issues/10776DataKinds promotion of String -> Symbol and Natural -> Nat2020-10-28T13:07:08ZhtebalakaDataKinds promotion of String -> Symbol and Natural -> NatExactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :...Exactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :: Y ('X "hello" 4)
```
I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.