GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:15:41Zhttps://gitlab.haskell.org/ghc/ghc//issues/14772Keep Role Annotations in the renamed syntax tree20190707T18:15:41ZlazacKeep Role Annotations in the renamed syntax treeCurrently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.
Keeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.
Minimal example:
A.hs
```hs
module A where
import B
data A x = A B
```
B.hs
```hs
module B where
import {# SOURCE #} A
data B = B (A ())
```
A.hsboot
```hs
{# LANGUAGE RoleAnnotations #}
module A where
type role A phantom  the role annotation is needed here
data A x
```
When inspecting the representation using the GHC API, the role is present in the parsed representation:
```
module A where  Parsed module
type role A phantom
data A x
```
But missing from the renamed one:
```
(data A x, [import (implicit) Prelude], Nothing, Nothing)  RenamedSource
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"Keep Role Annotations in the renamed syntax tree","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.\r\n\r\nKeeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.\r\n\r\nMinimal example:\r\n\r\nA.hs\r\n{{{#!hs\r\nmodule A where\r\nimport B\r\ndata A x = A B\r\n}}}\r\n\r\nB.hs\r\n{{{#!hs\r\nmodule B where\r\nimport {# SOURCE #} A\r\ndata B = B (A ())\r\n}}}\r\n\r\nA.hsboot\r\n{{{#!hs\r\n{# LANGUAGE RoleAnnotations #}\r\nmodule A where\r\ntype role A phantom  the role annotation is needed here\r\ndata A x\r\n}}}\r\n\r\nWhen inspecting the representation using the GHC API, the role is present in the parsed representation:\r\n\r\n{{{\r\nmodule A where  Parsed module\r\ntype role A phantom\r\ndata A x\r\n}}}\r\n\r\nBut missing from the renamed one:\r\n\r\n{{{\r\n(data A x, [import (implicit) Prelude], Nothing, Nothing)  RenamedSource\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >Currently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.
Keeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.
Minimal example:
A.hs
```hs
module A where
import B
data A x = A B
```
B.hs
```hs
module B where
import {# SOURCE #} A
data B = B (A ())
```
A.hsboot
```hs
{# LANGUAGE RoleAnnotations #}
module A where
type role A phantom  the role annotation is needed here
data A x
```
When inspecting the representation using the GHC API, the role is present in the parsed representation:
```
module A where  Parsed module
type role A phantom
data A x
```
But missing from the renamed one:
```
(data A x, [import (implicit) Prelude], Nothing, Nothing)  RenamedSource
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"Keep Role Annotations in the renamed syntax tree","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Currently role annotations are present in the parsed representation, but missing from the renamed version of the syntax tree. GHC should keep them instead. I found no evidence that this would be intended, we even have `rnRoleAnnots` that should return the renamed annotations.\r\n\r\nKeeping role annotations would help tooling to be consistent. For example, renaming the datatype should also rename its occurrence in the role annotation.\r\n\r\nMinimal example:\r\n\r\nA.hs\r\n{{{#!hs\r\nmodule A where\r\nimport B\r\ndata A x = A B\r\n}}}\r\n\r\nB.hs\r\n{{{#!hs\r\nmodule B where\r\nimport {# SOURCE #} A\r\ndata B = B (A ())\r\n}}}\r\n\r\nA.hsboot\r\n{{{#!hs\r\n{# LANGUAGE RoleAnnotations #}\r\nmodule A where\r\ntype role A phantom  the role annotation is needed here\r\ndata A x\r\n}}}\r\n\r\nWhen inspecting the representation using the GHC API, the role is present in the parsed representation:\r\n\r\n{{{\r\nmodule A where  Parsed module\r\ntype role A phantom\r\ndata A x\r\n}}}\r\n\r\nBut missing from the renamed one:\r\n\r\n{{{\r\n(data A x, [import (implicit) Prelude], Nothing, Nothing)  RenamedSource\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14858Typed hole subtitution search fails in the REPL20190707T18:15:18Zpaf31Typed hole subtitution search fails in the REPLIt seems as though type class defaulting might be happening before the search.
This finds only undefined:
`
> _traverse print "abc"
<interactive>:20:1: error:
• Found hole: _traverse :: (() > IO ()) > [Char] > t
Where: ‘t’ is a rigid type variable bound by
the inferred type of it :: t
at <interactive>:20:121
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc"
In an equation for ‘it’: it = _traverse print "abc"
• Relevant bindings include it :: t (bound at <interactive>:20:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
Annotating the return type helps, but we still don't find traverse_:
`
> _traverse print "abc" :: IO ()
<interactive>:22:1: error:
• Found hole: _traverse :: (() > IO ()) > [Char] > IO ()
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc" :: IO ()
In an equation for ‘it’: it = _traverse print "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:22:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
(note how print seems to have been defaulted to ())
Annotating the type of print helps:
`
> _traverse (print :: Char > IO ()) "abc" :: IO ()
<interactive>:23:1: error:
• Found hole: _traverse :: (Char > IO ()) > [Char] > IO ()
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression:
_traverse (print :: Char > IO ()) "abc" :: IO ()
In an equation for ‘it’:
it = _traverse (print :: Char > IO ()) "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:23:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
foldMap :: forall (t :: * > *).
Foldable t =>
forall m a. Monoid m => (a > m) > t a > m
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
mapM_ :: forall (t :: * > *) (m :: * > *) a b.
(Foldable t, Monad m) =>
(a > m b) > t a > m ()
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
traverse_ :: forall (t :: * > *) (f :: * > *) a b.
(Foldable t, Applicative f) =>
(a > f b) > t a > f ()
(imported from ‘Data.Foldable’)
`
This was found with 8.4.1rc.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha3 
 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":"Typed hole subtitution search fails in the REPL","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha3","keywords":["holes","substitutions","typed"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"It seems as though type class defaulting might be happening before the search.\r\n\r\nThis finds only undefined:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\"\r\n\r\n<interactive>:20:1: error:\r\n • Found hole: _traverse :: (() > IO ()) > [Char] > t\r\n Where: ‘t’ is a rigid type variable bound by\r\n the inferred type of it :: t\r\n at <interactive>:20:121\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\"\r\n In an equation for ‘it’: it = _traverse print \"abc\"\r\n • Relevant bindings include it :: t (bound at <interactive>:20:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\nAnnotating the return type helps, but we still don't find traverse_:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\" :: IO ()\r\n\r\n<interactive>:22:1: error:\r\n • Found hole: _traverse :: (() > IO ()) > [Char] > IO ()\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\" :: IO ()\r\n In an equation for ‘it’: it = _traverse print \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:22:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\n(note how print seems to have been defaulted to ())\r\n\r\nAnnotating the type of print helps:\r\n\r\n {{{#!text\r\n> _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n\r\n<interactive>:23:1: error:\r\n • Found hole: _traverse :: (Char > IO ()) > [Char] > IO ()\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression:\r\n _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n In an equation for ‘it’:\r\n it = _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:23:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n foldMap :: forall (t :: * > *).\r\n Foldable t =>\r\n forall m a. Monoid m => (a > m) > t a > m\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n mapM_ :: forall (t :: * > *) (m :: * > *) a b.\r\n (Foldable t, Monad m) =>\r\n (a > m b) > t a > m ()\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n traverse_ :: forall (t :: * > *) (f :: * > *) a b.\r\n (Foldable t, Applicative f) =>\r\n (a > f b) > t a > f ()\r\n (imported from ‘Data.Foldable’)\r\n }}}\r\n\r\nThis was found with 8.4.1rc.1.","type_of_failure":"OtherFailure","blocking":[]} >It seems as though type class defaulting might be happening before the search.
This finds only undefined:
`
> _traverse print "abc"
<interactive>:20:1: error:
• Found hole: _traverse :: (() > IO ()) > [Char] > t
Where: ‘t’ is a rigid type variable bound by
the inferred type of it :: t
at <interactive>:20:121
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc"
In an equation for ‘it’: it = _traverse print "abc"
• Relevant bindings include it :: t (bound at <interactive>:20:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
Annotating the return type helps, but we still don't find traverse_:
`
> _traverse print "abc" :: IO ()
<interactive>:22:1: error:
• Found hole: _traverse :: (() > IO ()) > [Char] > IO ()
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression: _traverse print "abc" :: IO ()
In an equation for ‘it’: it = _traverse print "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:22:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
`
(note how print seems to have been defaulted to ())
Annotating the type of print helps:
`
> _traverse (print :: Char > IO ()) "abc" :: IO ()
<interactive>:23:1: error:
• Found hole: _traverse :: (Char > IO ()) > [Char] > IO ()
Or perhaps ‘_traverse’ is misspelled, or not in scope
• In the expression: _traverse
In the expression:
_traverse (print :: Char > IO ()) "abc" :: IO ()
In an equation for ‘it’:
it = _traverse (print :: Char > IO ()) "abc" :: IO ()
• Relevant bindings include
it :: IO () (bound at <interactive>:23:1)
Valid substitutions include
mempty :: forall a. Monoid a => a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))
foldMap :: forall (t :: * > *).
Foldable t =>
forall m a. Monoid m => (a > m) > t a > m
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
mapM_ :: forall (t :: * > *) (m :: * > *) a b.
(Foldable t, Monad m) =>
(a > m b) > t a > m ()
(imported from ‘Prelude’
(and originally defined in ‘Data.Foldable’))
traverse_ :: forall (t :: * > *) (f :: * > *) a b.
(Foldable t, Applicative f) =>
(a > f b) > t a > f ()
(imported from ‘Data.Foldable’)
`
This was found with 8.4.1rc.1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha3 
 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":"Typed hole subtitution search fails in the REPL","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha3","keywords":["holes","substitutions","typed"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"It seems as though type class defaulting might be happening before the search.\r\n\r\nThis finds only undefined:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\"\r\n\r\n<interactive>:20:1: error:\r\n • Found hole: _traverse :: (() > IO ()) > [Char] > t\r\n Where: ‘t’ is a rigid type variable bound by\r\n the inferred type of it :: t\r\n at <interactive>:20:121\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\"\r\n In an equation for ‘it’: it = _traverse print \"abc\"\r\n • Relevant bindings include it :: t (bound at <interactive>:20:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\nAnnotating the return type helps, but we still don't find traverse_:\r\n\r\n {{{#!text\r\n> _traverse print \"abc\" :: IO ()\r\n\r\n<interactive>:22:1: error:\r\n • Found hole: _traverse :: (() > IO ()) > [Char] > IO ()\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression: _traverse print \"abc\" :: IO ()\r\n In an equation for ‘it’: it = _traverse print \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:22:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n }}}\r\n\r\n(note how print seems to have been defaulted to ())\r\n\r\nAnnotating the type of print helps:\r\n\r\n {{{#!text\r\n> _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n\r\n<interactive>:23:1: error:\r\n • Found hole: _traverse :: (Char > IO ()) > [Char] > IO ()\r\n Or perhaps ‘_traverse’ is misspelled, or not in scope\r\n • In the expression: _traverse\r\n In the expression:\r\n _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n In an equation for ‘it’:\r\n it = _traverse (print :: Char > IO ()) \"abc\" :: IO ()\r\n • Relevant bindings include\r\n it :: IO () (bound at <interactive>:23:1)\r\n Valid substitutions include\r\n mempty :: forall a. Monoid a => a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ (and originally defined in ‘GHC.Err’))\r\n foldMap :: forall (t :: * > *).\r\n Foldable t =>\r\n forall m a. Monoid m => (a > m) > t a > m\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n mapM_ :: forall (t :: * > *) (m :: * > *) a b.\r\n (Foldable t, Monad m) =>\r\n (a > m b) > t a > m ()\r\n (imported from ‘Prelude’\r\n (and originally defined in ‘Data.Foldable’))\r\n traverse_ :: forall (t :: * > *) (f :: * > *) a b.\r\n (Foldable t, Applicative f) =>\r\n (a > f b) > t a > f ()\r\n (imported from ‘Data.Foldable’)\r\n }}}\r\n\r\nThis was found with 8.4.1rc.1.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1Tao Hesighingnow@gmail.comTao Hesighingnow@gmail.comhttps://gitlab.haskell.org/ghc/ghc//issues/14968QuantifiedConstraints: Can't be RHS of type family instances20190707T18:14:51ZjosefQuantifiedConstraints: Can't be RHS of type family instancesHere's a type family that I tried to write using QuantifiedConstraints.
```hs
{# LANGUAGE TypeOperators #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
module QCTypeInstance where
import GHC.Exts (Constraint)
type family Functors (fs :: [(* > *) > * > *]) :: Constraint
type instance Functors '[] = (() :: Constraint)
type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
```
Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.
```
$ ../ghcwip/T2893/inplace/bin/ghcstage2 interactive QCTypeInstance.hs
GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )
QCTypeInstance.hs:13:15: error:
• Illegal polymorphic type:
forall (f :: * > *). Functor f => Functor (t f)
• In the type instance declaration for ‘Functors’

13  type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
 ^^^^^^^^
```
Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"QuantifiedConstraints: Can't be RHS of type family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a type family that I tried to write using QuantifiedConstraints.\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule QCTypeInstance where\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family Functors (fs :: [(* > *) > * > *]) :: Constraint\r\ntype instance Functors '[] = (() :: Constraint)\r\ntype instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n}}}\r\n\r\nUnfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.\r\n\r\n{{{\r\n$ ../ghcwip/T2893/inplace/bin/ghcstage2 interactive QCTypeInstance.hs \r\nGHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )\r\n\r\nQCTypeInstance.hs:13:15: error:\r\n • Illegal polymorphic type:\r\n forall (f :: * > *). Functor f => Functor (t f)\r\n • In the type instance declaration for ‘Functors’\r\n \r\n13  type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n  ^^^^^^^^\r\n}}}\r\n\r\nWould it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?","type_of_failure":"OtherFailure","blocking":[]} >Here's a type family that I tried to write using QuantifiedConstraints.
```hs
{# LANGUAGE TypeOperators #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE QuantifiedConstraints #}
module QCTypeInstance where
import GHC.Exts (Constraint)
type family Functors (fs :: [(* > *) > * > *]) :: Constraint
type instance Functors '[] = (() :: Constraint)
type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
```
Unfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.
```
$ ../ghcwip/T2893/inplace/bin/ghcstage2 interactive QCTypeInstance.hs
GHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )
QCTypeInstance.hs:13:15: error:
• Illegal polymorphic type:
forall (f :: * > *). Functor f => Functor (t f)
• In the type instance declaration for ‘Functors’

13  type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)
 ^^^^^^^^
```
Would it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"QuantifiedConstraints: Can't be RHS of type family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's a type family that I tried to write using QuantifiedConstraints.\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\nmodule QCTypeInstance where\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family Functors (fs :: [(* > *) > * > *]) :: Constraint\r\ntype instance Functors '[] = (() :: Constraint)\r\ntype instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n}}}\r\n\r\nUnfortunately, GHC complains that it's illegal to have polymorphism on the right hand side of a type instance definition.\r\n\r\n{{{\r\n$ ../ghcwip/T2893/inplace/bin/ghcstage2 interactive QCTypeInstance.hs \r\nGHCi, version 8.5.20180322: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling QCTypeInstance ( QCTypeInstance.hs, interpreted )\r\n\r\nQCTypeInstance.hs:13:15: error:\r\n • Illegal polymorphic type:\r\n forall (f :: * > *). Functor f => Functor (t f)\r\n • In the type instance declaration for ‘Functors’\r\n \r\n13  type instance Functors (t ': ts) = (forall f. Functor f => Functor (t f), Functors ts)\r\n  ^^^^^^^^\r\n}}}\r\n\r\nWould it be possible to lift this restriction and allow quantified constraints as right hand sides of type family instances? Or are there fundamental difficulties with what I'm trying to do?","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15014Exhaustivity check should suggest when COMPLETE could be helpful20190707T18:14:41ZEdward Z. YangExhaustivity check should suggest when COMPLETE could be helpful```
MacBookPro97:ghc ezyang$ cat A.hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern F :: a > b > (a, b)
pattern F x y = (x, y)
g :: (a, b) > (a, b)
g (F x y) = (x, y)
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp
A.hs:8:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: _

8  g (F x y) = (x, y)
 ^^^^^^^^^^^^^^^^^^
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version
The Glorious Glasgow Haskell Compilation System, version 8.5.20180304
```
Any time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Exhaustivity check should suggest when COMPLETE could be helpful","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\nMacBookPro97:ghc ezyang$ cat A.hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule A where\r\n\r\npattern F :: a > b > (a, b)\r\npattern F x y = (x, y)\r\n\r\ng :: (a, b) > (a, b)\r\ng (F x y) = (x, y)\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp\r\n\r\nA.hs:8:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘g’: Patterns not matched: _\r\n \r\n8  g (F x y) = (x, y)\r\n  ^^^^^^^^^^^^^^^^^^\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.5.20180304\r\n}}}\r\n\r\nAny time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.","type_of_failure":"OtherFailure","blocking":[]} >```
MacBookPro97:ghc ezyang$ cat A.hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern F :: a > b > (a, b)
pattern F x y = (x, y)
g :: (a, b) > (a, b)
g (F x y) = (x, y)
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp
A.hs:8:1: warning: [Wincompletepatterns]
Pattern match(es) are nonexhaustive
In an equation for ‘g’: Patterns not matched: _

8  g (F x y) = (x, y)
 ^^^^^^^^^^^^^^^^^^
MacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version
The Glorious Glasgow Haskell Compilation System, version 8.5.20180304
```
Any time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Exhaustivity check should suggest when COMPLETE could be helpful","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["PatternMatchWarnings","PatternSynonyms,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\nMacBookPro97:ghc ezyang$ cat A.hs\r\n{# LANGUAGE PatternSynonyms #}\r\nmodule A where\r\n\r\npattern F :: a > b > (a, b)\r\npattern F x y = (x, y)\r\n\r\ng :: (a, b) > (a, b)\r\ng (F x y) = (x, y)\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 c A.hs Wall fforcerecomp\r\n\r\nA.hs:8:1: warning: [Wincompletepatterns]\r\n Pattern match(es) are nonexhaustive\r\n In an equation for ‘g’: Patterns not matched: _\r\n \r\n8  g (F x y) = (x, y)\r\n  ^^^^^^^^^^^^^^^^^^\r\nMacBookPro97:ghc ezyang$ inplace/bin/ghcstage2 version\r\nThe Glorious Glasgow Haskell Compilation System, version 8.5.20180304\r\n}}}\r\n\r\nAny time the exhaustiveness checker throws up its hands and says that `_` is not matched, we ought to give a hint that this may have occurred due to pattern synonyms, and that the author of the pattern synonyms can help out by specifying a COMPLETE pragma.","type_of_failure":"OtherFailure","blocking":[]} >8.4.3https://gitlab.haskell.org/ghc/ghc//issues/15310Derive Generic1 instances for types of kind (k > *) > * that include applic...20190707T18:13:20ZcedricshockDerive Generic1 instances for types of kind (k > *) > * that include applications of the parameterThe `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k > *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.
It currently cannot derive an instance for
```hs
newtype Fix f = In (f (Fix f))
deriving (Generic1)
```
or for
```hs
data Child f = Child {
ordinal :: Int,
nickname :: f String
}
deriving (Generic1)
```
It's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 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":"Derive Generic1 instances for types of kind (k > *) > * that include applications of the parameter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["DeriveGeneric","Generic1"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k > *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.\r\n\r\nIt currently cannot derive an instance for\r\n\r\n{{{#!hs\r\nnewtype Fix f = In (f (Fix f))\r\n deriving (Generic1)\r\n}}}\r\n\r\nor for \r\n\r\n{{{#!hs\r\ndata Child f = Child {\r\n ordinal :: Int,\r\n nickname :: f String\r\n}\r\n deriving (Generic1)\r\n}}}\r\n\r\nIt's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.","type_of_failure":"OtherFailure","blocking":[]} >The `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k > *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.
It currently cannot derive an instance for
```hs
newtype Fix f = In (f (Fix f))
deriving (Generic1)
```
or for
```hs
data Child f = Child {
ordinal :: Int,
nickname :: f String
}
deriving (Generic1)
```
It's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 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":"Derive Generic1 instances for types of kind (k > *) > * that include applications of the parameter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["DeriveGeneric","Generic1"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"The `Generic1` class is polykinded. The `DeriveGeneric` extension can derive `Generic1` instances for types of kind `k > *` parameterized over a parameter with a kind other than `k ~ *`, but only if they don't apply the parameter to other types.\r\n\r\nIt currently cannot derive an instance for\r\n\r\n{{{#!hs\r\nnewtype Fix f = In (f (Fix f))\r\n deriving (Generic1)\r\n}}}\r\n\r\nor for \r\n\r\n{{{#!hs\r\ndata Child f = Child {\r\n ordinal :: Int,\r\n nickname :: f String\r\n}\r\n deriving (Generic1)\r\n}}}\r\n\r\nIt's possible to represent these types generically, either with composition that can include occurrences of the parameter or with new types that represent applications of the parameter.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15557Reduce type families in equations' RHS when testing equation compatibility20190707T18:04:08ZmniipReduce type families in equations' RHS when testing equation compatibilityThe reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 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":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf
There in Definition 8 in section 3.4 it states:
Definition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.
Examine the following families:
```hs
type family If (a :: Bool) (b :: k) (c :: k) :: k where
If False a b = b
If True a b = a
type family Eql (a :: k) (b :: k) :: Bool where
Eql a a = True
Eql _ _ = False
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing
Test a a = a
Test Nothing _ = Nothing
Test _ Nothing = Nothing
```
Applying the check to the equations 1 and 2 of `Test` we get:
unify(\<`Just x`, `Just y`\>, \<`a`, `a`\>) = Ω = \[`a` \> `Just x`, `y` \> `x`\]
Ω(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)
Therefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`
That doesn't happen:
```hs
> :t undefined :: p a > p (Test a a)
p a > p (Test a a)
```
Examining the IfaceAxBranches (cf #15546) we see:
```hs
axiom D:R:Test::
Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing
Test k a a = a
(incompatible indices: [0])
Test k 'Nothing _ = 'Nothing
Test k _ 'Nothing = 'Nothing
```
GHC did not consider the two equations compatible.
Digging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's [ticket:8423\#comment:80951](https://gitlab.haskell.org//ghc/ghc/issues/8423#note_80951), but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).
The family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).
This brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?
P.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:
```hs
type family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where
Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing
Test a a = If (Eql a a) a Nothing
Test Nothing a = If (Eql Nothing a) Nothing Nothing
Test a Nothing = If (Eql a Nothing) Nothing Nothing
```
This lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.
P.P.S: In [ticket:15546\#comment:158797](https://gitlab.haskell.org//ghc/ghc/issues/15546#note_158797) I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  FeatureRequest 
 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":"Reduce type families in equations' RHS when testing equation compatibility","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj"],"type":"FeatureRequest","description":"The reference I found for closed type families with compatible equations is: https://www.microsoft.com/enus/research/wpcontent/uploads/2016/07/popl137eisenberg.pdf\r\n\r\nThere in Definition 8 in section 3.4 it states:\r\n\r\nDefinition 8 (Compatibility implementation). The test for compatibility, written compat(p, q), checks that unify(lhsp, lhsq) = Ω implies Ω(rhsp) = Ω(rhsq). If unify(lhsp, lhsq) fails, compat(p, q) holds vacuously.\r\n\r\nExamine the following families:\r\n\r\n{{{#!hs\r\ntype family If (a :: Bool) (b :: k) (c :: k) :: k where\r\n If False a b = b\r\n If True a b = a\r\n\r\ntype family Eql (a :: k) (b :: k) :: Bool where\r\n Eql a a = True\r\n Eql _ _ = False\r\n\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql x y) (Just x) Nothing\r\n Test a a = a\r\n Test Nothing _ = Nothing\r\n Test _ Nothing = Nothing\r\n}}}\r\n\r\nApplying the check to the equations 1 and 2 of `Test` we get:\r\n\r\nunify(<`Just x`, `Just y`>, <`a`, `a`>) = Ω = [`a` > `Just x`, `y` > `x`]\r\n\r\nΩ(`a`) = `Just x` = `If (Eql x x) (Just x) Nothing` = Ω(`If (Eql x y) (Just x) Nothing`)\r\n\r\nTherefore the equations must be compatible, and when tidying `forall a. p a > p (Test a a)` the application should reduce to `forall a. p a > p a`\r\n\r\nThat doesn't happen:\r\n{{{#!hs\r\n> :t undefined :: p a > p (Test a a)\r\np a > p (Test a a)\r\n}}}\r\n\r\nExamining the IfaceAxBranches (cf #15546) we see:\r\n{{{#!hs\r\n axiom D:R:Test::\r\n Test a ('Just x) ('Just y) = If (Eql x y) ('Just x) 'Nothing\r\n Test k a a = a\r\n (incompatible indices: [0])\r\n Test k 'Nothing _ = 'Nothing\r\n Test k _ 'Nothing = 'Nothing\r\n}}}\r\n\r\nGHC did not consider the two equations compatible.\r\n\r\nDigging into why, I came across this ticket: #8423, in which a potentially unbounded (and indefinite) number of type family reductions was necessary to evidence Ω(rhsp) = Ω(rhsq). I don't claim to fully understand goldfire's ticket:8423#comment:10, but the issue is clear: reducing type families while doing a compartibility check might depend on other compatibility checks already being done, including a check depending on itself in which case we are interested in the biggest fixed point (why?).\r\n\r\nThe family here doesn't require any of that special consideration because `Eql x x` reduces right away without any compatibility checks, and `If` is essentially open (indeed making `If` open doesn't help anything).\r\n\r\nThis brings the question: is something like goldfire's described algorithm (or a simplification thereof) something we would like to have in GHC or is that too complex? What is the status on the implementation of that algorithm?\r\n\r\nP.S: An interesting workaround is adding an `If t c c = c` equation (compatible), and then writing `Test` as:\r\n{{{#!hs\r\ntype family Test (a :: Maybe k) (b :: Maybe k) :: Maybe k where\r\n Test (Just x) (Just y) = If (Eql (Just x) (Just y)) (Just x) Nothing\r\n Test a a = If (Eql a a) a Nothing\r\n Test Nothing a = If (Eql Nothing a) Nothing Nothing\r\n Test a Nothing = If (Eql a Nothing) Nothing Nothing\r\n}}}\r\n\r\nThis lets GHC discover the necessary equalities without reducing type families, yet erase the workaround'ed type family applications immediately.\r\n\r\nP.P.S: In ticket:15546#comment:4 I mixed up left and right, it's the RHS that should be/are not reduced. This probably confused SPJ a lot.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15639Surprising failure combining QuantifiedConstraints with Coercible20190707T18:03:38ZDavid FeuerSurprising failure combining QuantifiedConstraints with CoercibleI don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I don't understand what's going wrong here.
```hs
 Fishy.hs
{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r
yeahCoercible r = r
 Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:134
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)

8  yeah = yeahCoercible Coercion

```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n Fishy.hs\r\n{# language RankNTypes, QuantifiedConstraints, RoleAnnotations #}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) > r\r\nyeahCoercible r = r\r\n\r\n\r\n Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:134\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n \r\n8  yeah = yeahCoercible Coercion\r\n \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15707More liberally kinded coercions for newtypes20190707T18:03:21ZmniipMore liberally kinded coercions for newtypesConsider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```Consider the infinite data family (possible thanks to #12369):
```hs
data family I :: k > k
newtype instance I a = I0 (a)
newtype instance I a x = I1 (a x)
newtype instance I a x y = I2 (a x y)
newtype instance I a x y z = I3 (a x y z)
...
```
We end up with a family of etacontracted coercions:
```hs
forall (a :: *). a ~R I a
forall (a :: k > *). a ~R I a
forall (a :: k > l > *). a ~R I a
forall (a :: k > l > m > *). a ~R I a
...
```
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion `forall (a :: k). a ~R I a`
Maybe even do so by default: `newtype I a = I0 a` would create such a polykinded coercion. Though the `I0` data constructor and pattern would still only use the \*kinded restriction of it.
We could then recover other constructors with:
```hs
i1 :: a x > I a x
i1 = coerce
...
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15708Crossmodule SPECIALZE pragmas aren't typechecked in O020190707T18:03:21ZregnatCrossmodule SPECIALZE pragmas aren't typechecked in O0If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).
For example, given
```hs
 Foo.hs
module Foo where
foo :: a > a
foo = id

 Bar.hs
module Bar where
import Foo
{# SPECIALIZE foo :: Int > Bool #}
```
running `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:
```
Bar.hs:5:1: error:
• Couldn't match type ‘Bool’ with ‘Int’
Expected type: Int > Int
Actual type: Int > Bool
• In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}

5  {# SPECIALIZE foo :: Int > Bool #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Tested on ghc 8.6.1 and 8.4.3
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.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":"Crossmodule SPECIALZE pragmas aren't typechecked in O0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If a module defines a `SPECIALIZE` pragma for a value defined in another module, then the signature of this pragma won't be typecheck by `ghc O0` (but it will be if the `SPECIALIZE` pragma is in the same module as the value).\r\n\r\nFor example, given\r\n\r\n{{{#!hs\r\n Foo.hs\r\nmodule Foo where\r\n\r\nfoo :: a > a\r\nfoo = id\r\n\r\n\r\n\r\n Bar.hs\r\nmodule Bar where\r\n\r\nimport Foo\r\n\r\n{# SPECIALIZE foo :: Int > Bool #}\r\n}}}\r\n\r\nrunning `ghc make Bar.hs` will run fine, while `ghc make O2 Bar.hs` will complain:\r\n\r\n{{{\r\nBar.hs:5:1: error:\r\n • Couldn't match type ‘Bool’ with ‘Int’\r\n Expected type: Int > Int\r\n Actual type: Int > Bool\r\n • In the SPECIALISE pragma {# SPECIALIZE foo :: Int > Bool #}\r\n \r\n5  {# SPECIALIZE foo :: Int > Bool #}\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nTested on ghc 8.6.1 and 8.4.3","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/15989Adding extra quantified constraints leads to resolution failure20190707T18:02:08ZerorAdding extra quantified constraints leads to resolution failure```
{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
```
`ok` and `better` compile, but `bad` fails to resolve, despite having strictly more in the context than `ok`:
```
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^^^^^^^^^^^^
BadQC.hs:15:17: error:
• Could not deduce (Applicative (m y)) arising from a use of ‘pure’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the second argument of ‘fmap’, namely ‘(pure True)’
In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
```
Also:
 `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles — the error seems to require two quantified type variables
 `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an ambiguity error on the constraint, which makes sense; if I turn on `AllowAmbiguousTypes`, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same class hierarchy matters
 `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on `fmap` (but not `pure`) — which is the superclass doesn't seem to matter```
{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
```
`ok` and `better` compile, but `bad` fails to resolve, despite having strictly more in the context than `ok`:
```
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^^^^^^^^^^^^
BadQC.hs:15:17: error:
• Could not deduce (Applicative (m y)) arising from a use of ‘pure’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the second argument of ‘fmap’, namely ‘(pure True)’
In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
```
Also:
 `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles — the error seems to require two quantified type variables
 `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an ambiguity error on the constraint, which makes sense; if I turn on `AllowAmbiguousTypes`, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same class hierarchy matters
 `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on `fmap` (but not `pure`) — which is the superclass doesn't seem to matter8.6.3https://gitlab.haskell.org/ghc/ghc//issues/16154Wredundantconstraints: False positive20190707T18:01:16ZFumiaki KinoshitaWredundantconstraints: False positiveGHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundantconstraint.hs:24:1: warning: [Wredundantconstraints]
• Redundant constraints: (KnownNat 42, Capture 42 p)
• In the type signature for:
foo :: Foo 42

24  foo :: Foo 42
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"Wredundantconstraints: False positive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:\r\n\r\n{{{\r\nredundantconstraint.hs:24:1: warning: [Wredundantconstraints]\r\n • Redundant constraints: (KnownNat 42, Capture 42 p)\r\n • In the type signature for:\r\n foo :: Foo 42\r\n \r\n24  foo :: Foo 42\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:
```
redundantconstraint.hs:24:1: warning: [Wredundantconstraints]
• Redundant constraints: (KnownNat 42, Capture 42 p)
• In the type signature for:
foo :: Foo 42

24  foo :: Foo 42
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"Wredundantconstraints: False positive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC produces a warning for the attached source, although it won't compile if the suggested constraints are removed:\r\n\r\n{{{\r\nredundantconstraint.hs:24:1: warning: [Wredundantconstraints]\r\n • Redundant constraints: (KnownNat 42, Capture 42 p)\r\n • In the type signature for:\r\n foo :: Foo 42\r\n \r\n24  foo :: Foo 42\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16374Cannot deduce constraint from itself with polykinded type family20190707T18:00:20ZrolandCannot deduce constraint from itself with polykinded type familyCompiling
```hs
{# LANGUAGE PolyKinds, TypeFamilies #}
module Eq where
type family F a :: k where
withEq :: F Int ~ F Bool => a
withEq = undefined
```
gives an arguably confusing error message:
```
Eq.hs:7:11: error:
• Could not deduce: F Int ~ F Bool
from the context: F Int ~ F Bool
bound by the type signature for:
withEq :: forall k a. (F Int ~ F Bool) => a
at Eq.hs:7:1129
NB: ‘F’ is a noninjective type family
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘withEq’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: withEq :: F Int ~ F Bool => a
```
I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces headscratching.
Replacing `k` with `*` in the definition of `F` makes the error go away.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"Cannot deduce constraint from itself with polykinded type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds, TypeFamilies #}\r\n\r\nmodule Eq where\r\n\r\ntype family F a :: k where\r\n\r\nwithEq :: F Int ~ F Bool => a\r\nwithEq = undefined\r\n}}}\r\n\r\ngives an arguably confusing error message:\r\n\r\n{{{\r\nEq.hs:7:11: error:\r\n • Could not deduce: F Int ~ F Bool\r\n from the context: F Int ~ F Bool\r\n bound by the type signature for:\r\n withEq :: forall k a. (F Int ~ F Bool) => a\r\n at Eq.hs:7:1129\r\n NB: ‘F’ is a noninjective type family\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘withEq’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature: withEq :: F Int ~ F Bool => a\r\n}}}\r\n\r\nI'm not claiming this program should necessarily typecheck, but \"Cannot deduce X from the context X\" induces headscratching.\r\n\r\nReplacing `k` with `*` in the definition of `F` makes the error go away.","type_of_failure":"OtherFailure","blocking":[]} >Compiling
```hs
{# LANGUAGE PolyKinds, TypeFamilies #}
module Eq where
type family F a :: k where
withEq :: F Int ~ F Bool => a
withEq = undefined
```
gives an arguably confusing error message:
```
Eq.hs:7:11: error:
• Could not deduce: F Int ~ F Bool
from the context: F Int ~ F Bool
bound by the type signature for:
withEq :: forall k a. (F Int ~ F Bool) => a
at Eq.hs:7:1129
NB: ‘F’ is a noninjective type family
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘withEq’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: withEq :: F Int ~ F Bool => a
```
I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces headscratching.
Replacing `k` with `*` in the definition of `F` makes the error go away.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.6.3 
 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":"Cannot deduce constraint from itself with polykinded type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds, TypeFamilies #}\r\n\r\nmodule Eq where\r\n\r\ntype family F a :: k where\r\n\r\nwithEq :: F Int ~ F Bool => a\r\nwithEq = undefined\r\n}}}\r\n\r\ngives an arguably confusing error message:\r\n\r\n{{{\r\nEq.hs:7:11: error:\r\n • Could not deduce: F Int ~ F Bool\r\n from the context: F Int ~ F Bool\r\n bound by the type signature for:\r\n withEq :: forall k a. (F Int ~ F Bool) => a\r\n at Eq.hs:7:1129\r\n NB: ‘F’ is a noninjective type family\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘withEq’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature: withEq :: F Int ~ F Bool => a\r\n}}}\r\n\r\nI'm not claiming this program should necessarily typecheck, but \"Cannot deduce X from the context X\" induces headscratching.\r\n\r\nReplacing `k` with `*` in the definition of `F` makes the error go away.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/16786GHC suggests that infix operators might have the wrong number of arguments20190707T18:00:03ZChris SmithGHC suggests that infix operators might have the wrong number of arguments# Summary
GHC sometimes suggests that you have passed the wrong number of arguments to an infix operator.
# Steps to reproduce
Compile this code with GHC 8.6.5:
answer = map (foo ++ bar) "hello, world"
foo = toUpper
bar = take 10
The first error message says:
Test.hs:1:15: error:
• Couldn't match expected type ‘Char > b’ with actual type ‘[a1]’
• Possible cause: ‘(++)’ is applied to too many arguments
In the first argument of ‘map’, namely ‘(foo ++ bar)’
In the expression: map (foo ++ bar) "hello, world"
In an equation for ‘answer’:
answer = map (foo ++ bar) "hello, world"
• Relevant bindings include answer :: [b] (bound at Test.hs:1:1)
The suggestion that I have applied (++) to too many arguments is not a very likely one, since infix operators must take two arguments just by their syntax alone. I suppose it's possible that I intended to write an operator section, but it seems like a stretch.
# Expected behavior
I would expect this error message without the suggest that (++) is applied to too many arguments.
# Environment
* GHC version used: 8.6.5# Summary
GHC sometimes suggests that you have passed the wrong number of arguments to an infix operator.
# Steps to reproduce
Compile this code with GHC 8.6.5:
answer = map (foo ++ bar) "hello, world"
foo = toUpper
bar = take 10
The first error message says:
Test.hs:1:15: error:
• Couldn't match expected type ‘Char > b’ with actual type ‘[a1]’
• Possible cause: ‘(++)’ is applied to too many arguments
In the first argument of ‘map’, namely ‘(foo ++ bar)’
In the expression: map (foo ++ bar) "hello, world"
In an equation for ‘answer’:
answer = map (foo ++ bar) "hello, world"
• Relevant bindings include answer :: [b] (bound at Test.hs:1:1)
The suggestion that I have applied (++) to too many arguments is not a very likely one, since infix operators must take two arguments just by their syntax alone. I suppose it's possible that I intended to write an operator section, but it seems like a stretch.
# Expected behavior
I would expect this error message without the suggest that (++) is applied to too many arguments.
# Environment
* GHC version used: 8.6.5⊥https://gitlab.haskell.org/ghc/ghc//issues/16675Multiple occurrences of the same polykinded type don't unify20190531T16:14:15ZChristopher RodriguesMultiple occurrences of the same polykinded type don't unify# Summary
Multiple occurrences of the same polykinded type in a type signature are treated as distinct types, leading to type errors. Type inference creates different kind variables for each occurrence of the type, and won't unify them.
# Steps to reproduce
Compiling the following file, GHC reports an error.
~~~~haskell
{# LANGUAGE PolyKinds #}
{# OPTIONS_GHC fprintexplicitkinds #}
module Bug where
data Proxy a = P
data Indexed (f :: k > *) = I
idpi :: Indexed Proxy > Indexed Proxy
idpi x = x
~~~~
It infers the type `idpi :: forall k k1. Indexed k (Proxy k) > Indexed k1 (Proxy k1)`, and it reports an error at the expression `x` because it's returning the parameter type (with `k`) where the return type (with `k1`) is expected.
This is just a fancy id function, and I would have liked for GHC to infer `forall k. Indexed k (Proxy k) > Indexed k (Proxy k)`.
# Environment
* GHC version used: 8.6.5 (Stack lts13.22)# Summary
Multiple occurrences of the same polykinded type in a type signature are treated as distinct types, leading to type errors. Type inference creates different kind variables for each occurrence of the type, and won't unify them.
# Steps to reproduce
Compiling the following file, GHC reports an error.
~~~~haskell
{# LANGUAGE PolyKinds #}
{# OPTIONS_GHC fprintexplicitkinds #}
module Bug where
data Proxy a = P
data Indexed (f :: k > *) = I
idpi :: Indexed Proxy > Indexed Proxy
idpi x = x
~~~~
It infers the type `idpi :: forall k k1. Indexed k (Proxy k) > Indexed k1 (Proxy k1)`, and it reports an error at the expression `x` because it's returning the parameter type (with `k`) where the return type (with `k1`) is expected.
This is just a fancy id function, and I would have liked for GHC to infer `forall k. Indexed k (Proxy k) > Indexed k (Proxy k)`.
# Environment
* GHC version used: 8.6.5 (Stack lts13.22)https://gitlab.haskell.org/ghc/ghc//issues/16684Relax local equality check20190523T08:09:21ZIavor S. DiatchkiRelax local equality checkConsider the following example:
```haskell
{# Language RankNTypes, TypeFamilies #}
type family F a
q :: (forall b. (F b ~ Int) => (a,b)) > ()
q _ = ()
```
Currently GHC rejects this program as ambiguous. The reason is that during the ambiguity check, GHC needs to solve a constraint of the form:
```haskell
forall a. forall b. (F b ~ Int) => (a ~ alpha)
```
where `alpha` is a unification variable corresponding to the type parameter of `q` when used. At present, this constraint
cannot be solved, as the local assumption `F B ~ Int` causes `alpha` to be untouchable. In general, this is the safe thing to do, as in the presence of local assumptions unifying `alpha` with `a` might not be the most general solution (and, in fact, there may be *no* most general solution).
However, in this case it seems that the current rules are bit too conservative: the local assumption cannot affect the goal in any way, so `q` is not really ambiguous, and perhaps we can relax the current restrictions a bit. @simonpj proposed the following possible refinements [1]:
* (A) An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.
That loosens up `Note [Letbound skolems]` in `TcSMonad`, perhaps significantly. In particular, it woudl accept the example above.
The same email [1] proposed a second possiblity, (B), but it looks dodgy. So this ticket is about implementing (A).
References:
* [1] https://mail.haskell.org/pipermail/ghcdevs/2019May/017669.html
* [2] Note [Letbound skolems] in `TcSMonad`Consider the following example:
```haskell
{# Language RankNTypes, TypeFamilies #}
type family F a
q :: (forall b. (F b ~ Int) => (a,b)) > ()
q _ = ()
```
Currently GHC rejects this program as ambiguous. The reason is that during the ambiguity check, GHC needs to solve a constraint of the form:
```haskell
forall a. forall b. (F b ~ Int) => (a ~ alpha)
```
where `alpha` is a unification variable corresponding to the type parameter of `q` when used. At present, this constraint
cannot be solved, as the local assumption `F B ~ Int` causes `alpha` to be untouchable. In general, this is the safe thing to do, as in the presence of local assumptions unifying `alpha` with `a` might not be the most general solution (and, in fact, there may be *no* most general solution).
However, in this case it seems that the current rules are bit too conservative: the local assumption cannot affect the goal in any way, so `q` is not really ambiguous, and perhaps we can relax the current restrictions a bit. @simonpj proposed the following possible refinements [1]:
* (A) An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.
That loosens up `Note [Letbound skolems]` in `TcSMonad`, perhaps significantly. In particular, it woudl accept the example above.
The same email [1] proposed a second possiblity, (B), but it looks dodgy. So this ticket is about implementing (A).
References:
* [1] https://mail.haskell.org/pipermail/ghcdevs/2019May/017669.html
* [2] Note [Letbound skolems] in `TcSMonad`