GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:33:51Zhttps://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/10450Poor type error message when an argument is insufficently polymorphic2019-07-07T18:35:52ZsjcjoostenPoor type error message when an argument is insufficently polymorphicWhen pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
...When pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) -> Phantom y
foo (Phantom x) = Phantom (x+1)
-- trying to map foo over a list, this is the only way I can get it to work
typeAnnotatedMap :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap intList = case intList of
[] -> []
_ -> let (phead:ptail) = intList
in foo phead : typeAnnotatedMap ptail
```
The following are not accepted:
```hs
typeAnnotatedMap1 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap1 intList = case intList of
[] -> []
(phead:ptail) -> foo phead : typeAnnotatedMap1 ptail
typeAnnotatedMap2 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap2 [] = []
typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail
```
The current type error is something like:
```
Couldn't match type ‘x0’ with ‘x’
because type variable ‘x’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: [Phantom x]
```
More helpful would be something like:
```
Your pattern match bound the following types to a shared skolem variable:
ptail :: [Phantom x0] (bound at rankNtest.hs:11:25)
phead :: Phantom x0 (bound at rankNtest.hs:11:19)
You may have intended to use a "let" or "where" pattern-match instead.
```https://gitlab.haskell.org/ghc/ghc/-/issues/10341hs-boot files can have bogus declarations if they're not exported2019-07-07T18:36:30ZEdward Z. Yanghs-boot files can have bogus declarations if they're not exportedConsider:
```
-- A.hs-boot
module A(foo) where
foo :: A -> Int
data A = AC { bar :: Int } | CC
-- NB: A is not exported
-- B.hs
module B where
import {-# SOURCE #-} A
-- A.hs
module A(foo) where
import B
data A = AC { ...Consider:
```
-- A.hs-boot
module A(foo) where
foo :: A -> Int
data A = AC { bar :: Int } | CC
-- NB: A is not exported
-- B.hs
module B where
import {-# SOURCE #-} A
-- A.hs
module A(foo) where
import B
data A = AC { foo :: Int } | BC
```
GHC won't complain that `A` is incompatibly defined, since it's not exported.
Seems relatively harmless though.https://gitlab.haskell.org/ghc/ghc/-/issues/10150Suppress orphan instance warning per instance2019-07-07T18:37:19ZEdward Z. YangSuppress orphan instance warning per instanceIn the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there ...In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress orphan instance warning per instance","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":"FeatureRequest","description":"In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.\r\n\r\nAnnoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9981Potential typechecker regression in GHC 7.10.1RC2019-07-07T18:38:04ZHerbert Valerio Riedelhvr@gnu.orgPotential typechecker regression in GHC 7.10.1RCThe following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:
```hs
{-# LANGUAGE Rank2Types, TypeOperators #-}
module Foo where
type a :-> b = forall i . a i -> b i
class IFunctor f where
fmapI ...The following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:
```hs
{-# LANGUAGE Rank2Types, TypeOperators #-}
module Foo where
type a :-> b = forall i . a i -> b i
class IFunctor f where
fmapI :: (a :-> b) -> (f a :-> f b)
class (IFunctor m) => IMonad m where
returnI :: a :-> m a
bindI :: (a :-> m b) -> (m a :-> m b)
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(?>=) = flip bindI
```
```
$ ghci-7.8.4 -Wall Foo.hs
GHCi, version 7.8.4: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )
Ok, modules loaded: Control.IMonad.Core.
λ:2> :browse
type (:->) (a :: * -> *) (b :: * -> *) = forall i. a i -> b i
class IFunctor (f :: (* -> *) -> * -> *) where
fmapI :: (a :-> b) -> f a :-> f b
class IFunctor m => IMonad (m :: (* -> *) -> * -> *) where
returnI :: a i -> m a i
bindI :: (a :-> m b) -> m a :-> m b
(?>=) :: IMonad m => m a i -> (a :-> m b) -> m b i
```
vs.
```
$ ghci-7.10.0.20141227 -Wall Foo.hs
GHCi, version 7.10.0.20141227: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )
Foo.hs:15:14:
Couldn't match type ‘a i0 -> m b i0’ with ‘forall i1. a i1 -> m b i1’
Expected type: (a i0 -> m b i0) -> m a i -> m b i
Actual type: a :-> m b -> m a i -> m b i
Relevant bindings include (?>=) :: m a i -> a :-> m b -> m b i (bound at Foo.hs:15:1)
In the first argument of ‘flip’, namely ‘bindI’
In the expression: flip bindI
Failed, modules loaded: none.
λ:2>
```
I'm not sure though whether that module was valid to begin with...
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1-rc1 |
| Type | Bug |
| TypeOfFailure | ValidProgramRejected |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Potential typechecker regression in GHC 7.10.1RC","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"7.10.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE Rank2Types, TypeOperators #-}\r\n\r\nmodule Foo where\r\n\r\ntype a :-> b = forall i . a i -> b i\r\n\r\nclass IFunctor f where\r\n fmapI :: (a :-> b) -> (f a :-> f b)\r\n\r\nclass (IFunctor m) => IMonad m where\r\n returnI :: a :-> m a\r\n bindI :: (a :-> m b) -> (m a :-> m b)\r\n\r\n(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i\r\n(?>=) = flip bindI\r\n}}}\r\n\r\n{{{\r\n$ ghci-7.8.4 -Wall Foo.hs \r\nGHCi, version 7.8.4: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )\r\nOk, modules loaded: Control.IMonad.Core.\r\nλ:2> :browse\r\ntype (:->) (a :: * -> *) (b :: * -> *) = forall i. a i -> b i\r\nclass IFunctor (f :: (* -> *) -> * -> *) where\r\n fmapI :: (a :-> b) -> f a :-> f b\r\nclass IFunctor m => IMonad (m :: (* -> *) -> * -> *) where\r\n returnI :: a i -> m a i\r\n bindI :: (a :-> m b) -> m a :-> m b\r\n(?>=) :: IMonad m => m a i -> (a :-> m b) -> m b i\r\n}}}\r\n\r\nvs.\r\n\r\n{{{\r\n$ ghci-7.10.0.20141227 -Wall Foo.hs \r\nGHCi, version 7.10.0.20141227: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )\r\n\r\nFoo.hs:15:14:\r\n Couldn't match type ‘a i0 -> m b i0’ with ‘forall i1. a i1 -> m b i1’\r\n Expected type: (a i0 -> m b i0) -> m a i -> m b i\r\n Actual type: a :-> m b -> m a i -> m b i\r\n Relevant bindings include (?>=) :: m a i -> a :-> m b -> m b i (bound at Foo.hs:15:1)\r\n In the first argument of ‘flip’, namely ‘bindI’\r\n In the expression: flip bindI\r\nFailed, modules loaded: none.\r\nλ:2> \r\n}}}\r\n\r\nI'm not sure though whether that module was valid to begin with...","type_of_failure":"ValidProgramRejected","blocking":[]} -->8.4.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/9756Warn about unnecessary unsafeCoerce2019-07-07T18:39:11ZDavid FeuerWarn about unnecessary unsafeCoerce`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.
<details><summar...`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| 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":"Warn about unnecessary unsafeCoerce","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.9","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9518Improve error message for unacceptable role annotations2023-12-06T21:12:16ZdmccleanImprove error message for unacceptable role annotationsIt would be nice if this message:
```
Role mismatch on variable a:
Annotation says representational but role nominal is required
while checking a role annotation for `Point'
```
Could be extended to say where the requirement arises.
...It would be nice if this message:
```
Role mismatch on variable a:
Annotation says representational but role nominal is required
while checking a role annotation for `Point'
```
Could be extended to say where the requirement arises.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.8.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Improve error message for unacceptable role annotations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It would be nice if this message:\r\n\r\n{{{\r\nRole mismatch on variable a:\r\n Annotation says representational but role nominal is required\r\nwhile checking a role annotation for `Point'\r\n}}}\r\n\r\nCould be extended to say where the requirement arises.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/8516Add (->) representation and the Invariant class to GHC.Generics2019-07-07T18:44:42ZnfrisbyAdd (->) representation and the Invariant class to GHC.GenericsWe currently disallow any use of the parameter in the domain of (-\>).
```
newtype F a = F ((a -> Int) -> Int) deriving Generic1
<interactive>:4:38:
Can't make a derived instance of `Generic1 (F g)':
Constructor `F' must use ...We currently disallow any use of the parameter in the domain of (-\>).
```
newtype F a = F ((a -> Int) -> Int) deriving Generic1
<interactive>:4:38:
Can't make a derived instance of `Generic1 (F g)':
Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->)
In the data declaration for `F'
```
!DeriveFunctor succeeds for this F.
I'd like to add this representation type to GHC.Generics and !DeriveGeneric.
```
newtype (f :->: g) a = FArrow1 (f a -> g a)
```
We could then represent the first example above. We could also derive the more interesting Generic1 (F g).
```
newtype F g a = F (g a -> Int) deriving Generic1
type instance Rep1 (F g) = Rec1 g :->: Rec0 Int
instance Generic1 (F g) where
to x = F $ unRec0 . unArrow1 x . Rec1
from (F x) = FArrow1 $ Rec0 . x . unRec1
```
Admittedly, there's not many generic definitions impeded by not having (:-\>:). Contra- and in-variant types are uncommon.
I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.
```
class Invariant t where
invmap :: (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant f _ = fmap f
instance (Invariant f,Invariant g) => Invariant (FArrow f g) where
invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co
```
(Of course, Invariant should be a super class of Functor. :/ )
Now we can handle quite involved examples:
```
newtype F g h a = F (g (h a)) deriving Generic1
instance Invariant g => Generic1 (F g h) where
to x = invmap unRec1 Rec1 $ unComp1 x
from (F x) = Comp1 $ invmap Rec1 unRec1
```
All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Add (->) representation and the Invariant class to GHC.Generics","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"We currently disallow any use of the parameter in the domain of (->).\r\n\r\n{{{\r\nnewtype F a = F ((a -> Int) -> Int) deriving Generic1\r\n\r\n<interactive>:4:38:\r\n Can't make a derived instance of `Generic1 (F g)':\r\n Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->)\r\n In the data declaration for `F'\r\n}}}\r\n\r\n!DeriveFunctor succeeds for this F.\r\n\r\nI'd like to add this representation type to GHC.Generics and !DeriveGeneric.\r\n\r\n{{{\r\nnewtype (f :->: g) a = FArrow1 (f a -> g a)\r\n}}}\r\n\r\nWe could then represent the first example above. We could also derive the more interesting Generic1 (F g).\r\n\r\n{{{\r\nnewtype F g a = F (g a -> Int) deriving Generic1\r\n\r\ntype instance Rep1 (F g) = Rec1 g :->: Rec0 Int\r\n\r\ninstance Generic1 (F g) where\r\n to x = F $ unRec0 . unArrow1 x . Rec1\r\n from (F x) = FArrow1 $ Rec0 . x . unRec1\r\n}}}\r\n\r\nAdmittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.\r\n\r\nI'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.\r\n\r\n{{{\r\nclass Invariant t where\r\n invmap :: (a -> b) -> (b -> a) -> t a -> t b\r\n\r\ninvmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b\r\ninvmap_covariant f _ = fmap f\r\n\r\ninstance (Invariant f,Invariant g) => Invariant (FArrow f g) where\r\n invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co\r\n}}}\r\n\r\n(Of course, Invariant should be a super class of Functor. :/ )\r\n\r\nNow we can handle quite involved examples:\r\n\r\n{{{\r\nnewtype F g h a = F (g (h a)) deriving Generic1\r\n\r\ninstance Invariant g => Generic1 (F g h) where\r\n to x = invmap unRec1 Rec1 $ unComp1 x\r\n from (F x) = Comp1 $ invmap Rec1 unRec1\r\n}}}\r\n\r\nAll of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/8447A combination of type-level comparison and subtraction does not work for 02019-07-07T18:45:02ZnushioA combination of type-level comparison and subtraction does not work for 0The following function on type level naturals
```
Diff x y = If (x <=? y) (y-x) (x-y)
```
does not work when either x or y is 0.
https://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e653a27/type-nats/int-bug.hs
...The following function on type level naturals
```
Diff x y = If (x <=? y) (y-x) (x-y)
```
does not work when either x or y is 0.
https://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e653a27/type-nats/int-bug.hs
I've tested this code on ghc 7.7.20130926 since I couldn't build the really latest ghc. I'm sorry if it is already fixed on the ghc head.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"A combination of type-level comparison and subtraction does not work for 0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following function on type level naturals\r\n\r\n{{{\r\n Diff x y = If (x <=? y) (y-x) (x-y)\r\n}}}\r\n\r\ndoes not work when either x or y is 0.\r\n\r\nhttps://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e653a27/type-nats/int-bug.hs\r\n\r\n\r\nI've tested this code on ghc 7.7.20130926 since I couldn't build the really latest ghc. I'm sorry if it is already fixed on the ghc head.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5267Missing type checks for arrow command combinators2019-07-07T18:56:08ZpetegMissing type checks for arrow command combinatorsIs this expected to work?
```
{-# LANGUAGE Arrows #-}
module T where
import Prelude
import Control.Arrow
t = proc () ->
do rec x <- arr id <<< (| (arr id) (returnA -< x) |)
returnA -< x
t' = proc x ->
do x <- arr id...Is this expected to work?
```
{-# LANGUAGE Arrows #-}
module T where
import Prelude
import Control.Arrow
t = proc () ->
do rec x <- arr id <<< (| (arr id) (returnA -< x) |)
returnA -< x
t' = proc x ->
do x <- arr id <<< (| (arr id) (returnA -< x) |)
returnA -< x
t'' = proc x ->
do x <- arr id <<< (| (arr id) (returnA -< 3) |)
returnA -< x
t''' = proc x -> arr id <<< (| (arr id) (returnA -< 3) |)
```
I get:
```
/tmp/T.hs:8:18:
The type of the first argument of a command form has the wrong shape
Argument type: t_tX
In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
rec {x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))}
/tmp/T.hs:12:14:
The type of the first argument of a command form has the wrong shape
Argument type: t_tG
In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))
In the expression:
proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< x))|));
returnA -< x }
/tmp/T.hs:16:14:
The type of the first argument of a command form has the wrong shape
Argument type: t_tq
In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In the expression:
proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|));
returnA -< x }
/tmp/T.hs:19:18:
The type of the first argument of a command form has the wrong shape
Argument type: t_k
In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In the expression:
proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In an equation for `t'''':
t''' = proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------------- |
| Version | 7.0.3 |
| Type | Bug |
| TypeOfFailure | ValidProgramRejected |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Arrow command combinators","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.0.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Is this expected to work?\r\n\r\n{{{\r\n{-# LANGUAGE Arrows #-}\r\nmodule T where\r\n\r\nimport Prelude\r\nimport Control.Arrow\r\n\r\nt = proc () ->\r\n do rec x <- arr id <<< (| (arr id) (returnA -< x) |)\r\n returnA -< x\r\n\r\nt' = proc x ->\r\n do x <- arr id <<< (| (arr id) (returnA -< x) |)\r\n returnA -< x\r\n\r\nt'' = proc x ->\r\n do x <- arr id <<< (| (arr id) (returnA -< 3) |)\r\n returnA -< x\r\n\r\nt''' = proc x -> arr id <<< (| (arr id) (returnA -< 3) |)\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\n/tmp/T.hs:8:18:\r\n The type of the first argument of a command form has the wrong shape\r\n Argument type: t_tX\r\n In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))\r\n In a stmt of a 'do' expression:\r\n x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))\r\n In a stmt of a 'do' expression:\r\n rec {x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))}\r\n\r\n/tmp/T.hs:12:14:\r\n The type of the first argument of a command form has the wrong shape\r\n Argument type: t_tG\r\n In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))\r\n In a stmt of a 'do' expression:\r\n x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))\r\n In the expression:\r\n proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< x))|));\r\n returnA -< x }\r\n\r\n/tmp/T.hs:16:14:\r\n The type of the first argument of a command form has the wrong shape\r\n Argument type: t_tq\r\n In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))\r\n In a stmt of a 'do' expression:\r\n x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|))\r\n In the expression:\r\n proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|));\r\n returnA -< x }\r\n\r\n/tmp/T.hs:19:18:\r\n The type of the first argument of a command form has the wrong shape\r\n Argument type: t_k\r\n In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))\r\n In the expression:\r\n proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))\r\n In an equation for `t'''':\r\n t''' = proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))\r\n}}}\r\n","type_of_failure":"ValidProgramRejected","blocking":[]} -->8.0.1Ross Patersonr.paterson@city.ac.ukRoss Patersonr.paterson@city.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/4020Please consider adding support for local type synonyms2019-07-07T19:01:04Znr@eecs.harvard.eduPlease consider adding support for local type synonymsI would really like to be able to put a type synonym in a where clause. I'm willing to specify `LANGUAGE ScopedTypeVariables, LiberalTypeSynonyms`.
For an example use case, please see line 202 of the attachment.
<details><summary>Trac ...I would really like to be able to put a type synonym in a where clause. I'm willing to specify `LANGUAGE ScopedTypeVariables, LiberalTypeSynonyms`.
For an example use case, please see line 202 of the attachment.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 6.12.2 |
| 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":"Please consider adding support for nested type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.12.2","keywords":["synonym","type"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I would really like to be able to put a type synonym in a where clause. I'm willing to specify {{{LANGUAGE ScopedTypeVariables, LiberalTypeSynonyms}}}.\r\n\r\nFor an example use case, please see line 202 of the attachment.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/1928Confusing type error message2022-03-07T06:48:02ZjosefConfusing type error messageThe following code (which is part of a bigger module) needs scoped type variables to compile.
```
run_state :: forall a s. State s a -> s -> (a,s)
run_state m s = observe_monad unit_op bind_op m where
unit_op v = (v,s)
bind...The following code (which is part of a bigger module) needs scoped type variables to compile.
```
run_state :: forall a s. State s a -> s -> (a,s)
run_state m s = observe_monad unit_op bind_op m where
unit_op v = (v,s)
bind_op :: BindOp (StateE s) a (a,s)
bind_op Get k = run_state (k s) s
bind_op (Put s1) k = run_state (k ()) s1
```
However, forgetting to turn on scoped type variables will give a very confusing error message:
```
Unimo.hs:56:36:
Couldn't match expected type `s1' against inferred type `s'
`s1' is a rigid type variable bound by
the type signature for `bind_op' at Unimo.hs:55:28
`s' is a rigid type variable bound by
the type signature for `run_state' at Unimo.hs:52:22
In the first argument of `k', namely `s'
In the first argument of `run_state', namely `(k s)'
In the expression: run_state (k s) s
```
Line 52 is the type signature of run_state and line 55 is the type signature of bind_op. The error message talks about a type variable \`s1' which isn't mentioned anywhere. I guess the reason for this is that we have name collision and this is ghc's way of trying to tell the two variables apart. I don't think it works that well though. But I'm afraid I don't have any suggestion on how to make it better.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Confusing type error message","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.8.1","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"The following code (which is part of a bigger module) needs scoped type variables to compile.\r\n\r\n{{{\r\nrun_state :: forall a s. State s a -> s -> (a,s)\r\nrun_state m s = observe_monad unit_op bind_op m where\r\n unit_op v = (v,s)\r\n bind_op :: BindOp (StateE s) a (a,s)\r\n bind_op Get k = run_state (k s) s\r\n bind_op (Put s1) k = run_state (k ()) s1\r\n}}}\r\nHowever, forgetting to turn on scoped type variables will give a very confusing error message:\r\n{{{\r\nUnimo.hs:56:36:\r\n Couldn't match expected type `s1' against inferred type `s'\r\n `s1' is a rigid type variable bound by\r\n the type signature for `bind_op' at Unimo.hs:55:28\r\n `s' is a rigid type variable bound by\r\n the type signature for `run_state' at Unimo.hs:52:22\r\n In the first argument of `k', namely `s'\r\n In the first argument of `run_state', namely `(k s)'\r\n In the expression: run_state (k s) s\r\n}}}\r\nLine 52 is the type signature of run_state and line 55 is the type signature of bind_op. The error message talks about a type variable `s1' which isn't mentioned anywhere. I guess the reason for this is that we have name collision and this is ghc's way of trying to tell the two variables apart. I don't think it works that well though. But I'm afraid I don't have any suggestion on how to make it better.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/1894Add a total order on type constructors2019-07-07T19:11:10ZguestAdd a total order on type constructorsSeveral proposals for ExtensibleRecords can be implemented as libraries if type constructors can be ordered globally.
This proposal is to add built-in types:
```
data LabelLT
data LabelEQ
data LabelGT
type family LabelCMP
```
such tha...Several proposals for ExtensibleRecords can be implemented as libraries if type constructors can be ordered globally.
This proposal is to add built-in types:
```
data LabelLT
data LabelEQ
data LabelGT
type family LabelCMP
```
such that, for any two datatypes
```
data N = N
data M = M
```
the instance `LabelCMP N M` takes one of the values `LabelLT, LabelEQ, LabelGT` depending on the lexicographic ordering on the fully-qualified names of `N` and `M`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.8.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Multiple |
| Architecture | Multiple |
</details>
<!-- {"blocked_by":[],"summary":"Add a total order on type constructors","status":"New","operating_system":"Multiple","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.8.1","keywords":[],"differentials":[],"test_case":"","architecture":"Multiple","cc":[""],"type":"FeatureRequest","description":"Several proposals for ExtensibleRecords can be implemented as libraries if type constructors can be ordered globally.\r\n\r\nThis proposal is to add built-in types:\r\n{{{\r\ndata LabelLT\r\ndata LabelEQ\r\ndata LabelGT\r\ntype family LabelCMP\r\n}}}\r\nsuch that, for any two datatypes\r\n{{{\r\ndata N = N\r\ndata M = M\r\n}}}\r\nthe instance {{{LabelCMP N M}}} takes one of the values {{{LabelLT, LabelEQ, LabelGT}}} depending on the lexicographic ordering on the fully-qualified names of {{{N}}} and {{{M}}}.\r\n\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/589Various poor type error messages2022-03-07T06:46:15ZPeter A Jonsson [pj@ludd.ltu.se]Various poor type error messagesHello,
I read the summary of the survey and noticed you wanted feedback on
where error messages could be improved. I looked up some (simple)
examples of type errors and ran them through ghc. I do not make any
claims to be an HCI expert,...Hello,
I read the summary of the survey and noticed you wanted feedback on
where error messages could be improved. I looked up some (simple)
examples of type errors and ran them through ghc. I do not make any
claims to be an HCI expert, just a mere mortal with an opinion.
**Type error 1**
Code:
```
module Test2 where
fib n = if (3 > n) then 1 else (fib (n - 1) + fib (n - 2))
k = fib 's'
```
Error message:
```
Test2.hs:4:
No instance for (Num Char)
arising from use of `fib' at Test2.hs:4
In the definition of `k': k = fib 's'
```
This isn't a bad error message in my humble opinion, it does pinpoint
that I'm doing something wrong in line 4, and that there isn't an
instance for Num Char doesn't come as a surprise. However I think it
could have been more helpful by telling me that I tried to pass a Char
to a function which expected an (Ord a, Num a) =\> a as its parameter.
**Type error 2**
Code:
```
module Test4 where
k :: Int -> Int
k l = 2.0*l
```
Error message:
```
Test4.hs:4:
No instance for (Fractional Int)
arising from the literal `2.0' at Test4.hs:4
In the first argument of `(*)', namely `2.0'
In the definition of `k': k l = 2.0 * l
```
One reason this kind of error could happen is an inexperienced user
declaring the wrong type for his function, or not knowing that 2.0
would be interpreted as a Fractional.
**Type error 3**
Code:
```
module Test7 where
len' xs = head (xs) + (length xs)
o = len' "GH"
```
Error message:
```
Test7.hs:4:
Couldn't match `Int' against `Char'
Expected type: [Int]
Inferred type: [Char]
In the first argument of `len'', namely `"GH"'
In the definition of `o': o = len' "GH"
```
I ran this through Hugs version November 2002 and got this error
message:
```
ERROR "Test7.hs":4 - Type error in application
*** Expression : len' "GH"
*** Term : "GH"
*** Type : String
*** Does not match : [Int]
```
I find the Hugs message more clear, but that might be my background.
**Type error 4**
Code:
```
module Test8 where
f = head 3
```
Error message:
```
Test8.hs:3:
No instance for (Num [a])
arising from the literal `3' at Test8.hs:3
Possible cause: the monomorphism restriction applied to the following:
f :: a (bound at Test8.hs:3)
Probable fix: give these definition(s) an explicit type signature
In the first argument of `head', namely `3'
In the definition of `f': f = head 3
```
This one I find outright scary. For "wrong = div 3 8 + 1/2" it gives
an error message that somewhat helps me guess the error, but the above
doesn't even come close to helping me.
/ Peterhttps://gitlab.haskell.org/ghc/ghc/-/issues/345GADT - fundep interaction2019-07-07T19:18:23ZbringGADT - fundep interaction```
GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used...```
GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used to figure out the result type.
{-# OPTIONS_GHC -fglasgow-exts #-}
data Succ n
data Zero
class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)
infixr 5 :::
data List :: * -> * -> * where
Nil :: List a Zero
(:::) :: a -> List a n -> List a (Succ n)
append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys
{-
GHC 6.4 says:
Couldn't match the rigid variable `y' against `Succ z'
`y' is bound by the type signature for `append'
Expected type: List a y
Inferred type: List a (Succ z)
In the expression: x ::: (append xs ys)
In the definition of `append': append (x ::: xs) ys
= x ::: (append xs ys)
-}
```Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/344arrow notation: incorrect scope of existential dictionaries2021-03-12T11:26:40Znobodyarrow notation: incorrect scope of existential dictionaries```
ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
cgPanic
deref{v a1yz}
static binds for:
local binds for:
SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
initC: srt
...```
ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
cgPanic
deref{v a1yz}
static binds for:
local binds for:
SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
initC: srt
Please report it as a compiler bug to
glasgow-haskell-bugs@haskell.org,
or http://sourceforge.net/projects/ghc/.
I've attached a test driver that can reproduce the problem.
-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>
```8.0.1Ross Patersonr.paterson@city.ac.ukRoss Patersonr.paterson@city.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/19634Implement type family reduction via term-level functions2023-06-30T20:26:43ZRinat Striungislazybonesxp@gmail.comImplement type family reduction via term-level functions## Motivation
Today I see two problems:
1. Type family reduction could be painfully slow.
In a complex case (type-level parser) rewriter took \~ 50% compilation time.
[Example](https://gist.github.com/Haskell-mouse/b05db12de9e9...## Motivation
Today I see two problems:
1. Type family reduction could be painfully slow.
In a complex case (type-level parser) rewriter took \~ 50% compilation time.
[Example](https://gist.github.com/Haskell-mouse/b05db12de9e9fdc8cfa9b02f436eccc0#file-1profilingwopatch-txt).
2. Writing base type families could cause one of two unwanted consequences:
1. In the case of adding them as built-in type families code base of GHC could be terribly grown.
[First char kind MR for example](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3598).
This MR includes many useful type families, but it was decided to make a smaller MR with only a few TFs to
avoid increasing GHC codebase for \~ 2000 lines mostly because of TFs.
2. Adding them via plugins is a painful process for developers at least because they have to track all changes in unstable GHC plugin API.
In both cases, developers have to learn many implementation details and internals of GHC.
## Proposal
I want to add a new **TYPEFUN** pragma, which works in the following way:
```type IsAlphaNum :: Char -> Bool
type family IsAlphaNum c
{-# TYPEFUN IsAlphaNum = Data.Char.isAlphaNum #-}
```
1. This pragma says which term-level function use for reducing type family.
2. It reduces only when inputs contain no type variables.
3. It works only when all types (both arguments and result) are promotable in any way.
The main idea is to use pre-compiled to bytecode term-level functions
in process of type checking which should solve both problems from the motivation part:
accelerate type family reduction and make writing TFs much easier.https://gitlab.haskell.org/ghc/ghc/-/issues/19396Surprising lack of generalisation using MonoLocalBinds2024-03-16T18:34:37ZTom EllisSurprising lack of generalisation using MonoLocalBinds## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic ...## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on Haskell-Cafe](https://mail.haskell.org/pipermail/haskell-cafe/2021-February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- This code came up in the context of writing a parser, but that's
-- not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
| DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
-- Does not type check
pFG1 :: Parser B -> Parser (D B)
pFG1 pBArg = pBD GF AP <|> pBD DF AM
where pBD f p = f p <$> pBArg
-- Does type check
pFG2 :: Parser B -> Parser (D B)
pFG2 pBArg = pBD GF AP <|> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
-- Does not type check
pFG3 :: forall b. Parser b -> Parser (D b)
pFG3 pBArg = pBD GF AP <|> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
-- The specifics of the parser don't matter
data Parser a = Parser
(<|>) :: Parser a -> Parser a -> Parser a
(<|>) _ _ = Parser
(<$>) :: (a -> b) -> Parser a -> Parser b
(<$>) _ _ = Parser
```https://gitlab.haskell.org/ghc/ghc/-/issues/17934Consider using specificity to disambiguate quantified constraints2021-02-21T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having ...**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type -> Constraint) where
Some :: c a => a -> Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show` -- maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a -> String` is the default method implementation for `show`. When type-checking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the top-level instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instance-lookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (non-quantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1` -- just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be non-quantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a non-quantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be set-like, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc/-/issues/17226Quantified constraints which specify associated type instances2023-07-05T22:08:56Zsheafsam.derbyshire@gmail.comQuantified constraints which specify associated type instancesI have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:
...I have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:
```haskell
class C a where
type T a :: Type
...
```
From what I understand, a quantified constraint of the form ```( forall a. C a => C (f a) )``` will be soluble when there is an instance of the form
```haskell
instance forall a. C a => C (f a)
```
My suggestion is to provide the ability to specify quantified constraints which restrict the associated type family instance declarations. In this case, we might want to insist upon the equation `type T (f a) = f (T a)`. One possible notation would use tuple and equality constraints (mirroring how one would encode this using `Dict`):
```haskell
forall a. C a => ( C (f a), T (f a) ~ f (T a) )
```
In solving this quantified constraint, we would discard all class instances which are not of the following form:
```haskell
instance forall a. C a => C (f a) where
type T (f a) = f (T a)
```
(I don't know how flexible we can afford to be in verifying this property, e.g. if the type family instance equations are not exactly as specified by the equality constraint but are equivalent to them, say after applying substitutions or using other equality constraints that might be available.)
### Example
To illustrate, I was working with the `Syntactic` type class
```haskell
class Syntactic a where
type Internal a
toAST :: a -> AST (Internal a)
fromAST :: AST (Internal a) -> a
```
and I wanted to restrict attention to functors `F` that are compatible with this type class, i.e. which have an instance declaration of the form
```haskell
instance Syntactic a => Syntactic (F a) where
type Internal (F a) = F (Internal a)
```
However, while I can write a quantified constraint `forall a. Syntactic a => Syntactic (f a)`, I cannot specify the additional requirement on the associated type family instance equation, so GHC will complain at use-sites:
```
* Could not deduce: Internal (f a) ~ f (Internal a)
```
This can be worked around using `Dict ( Syntactic (f a), Internal (f a) ~ f (Internal a) )`, unfortunately forgoing the use of quantified constraints and introducing indirections (requiring matching on `Dict` to make the instances visible to GHC). Other than that I don't know of any tricks to bypass this limitation, but I may well be missing something (quite likely, as I don't have much experience with quantified constraints).