GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:15:17Zhttps://gitlab.haskell.org/ghc/ghc//issues/14861QuantifiedConstraints: Can't use forall'd variable in context20190707T18:15:17ZRyan ScottQuantifiedConstraints: Can't use forall'd variable in contextThis fails to typecheck, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableI...This fails to typecheck, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
data ECC1 :: (Type > Constraint) > (Type > Type) > Type > Type where
ECC1 :: c p => f p > ECC1 c f p
class Foldable' f where
foldMap' :: Monoid m => (a > m) > f a > m
instance (forall p. c p => Foldable' f) => Foldable' (ECC1 c f) where
foldMap' f (ECC1 x) = foldMap' f x
instance Foldable' [] where
foldMap' = foldMap
test :: ECC1 Show [] Ordering > Ordering
test = foldMap' id
```
```
$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:18:25: error:
• Could not deduce: c p0 arising from a use of ‘foldMap'’
from the context: forall p. c p => Foldable' f
bound by the instance declaration at Bug.hs:17:1063
or from: Monoid m
bound by the type signature for:
foldMap' :: forall m a. Monoid m => (a > m) > ECC1 c f a > m
at Bug.hs:18:310
or from: c a
bound by a pattern with constructor:
ECC1 :: forall (f :: * > *) p (c :: * > Constraint).
c p =>
f p > ECC1 c f p,
in an equation for ‘foldMap'’
at Bug.hs:18:1520
• In the expression: foldMap' f x
In an equation for ‘foldMap'’: foldMap' f (ECC1 x) = foldMap' f x
In the instance declaration for ‘Foldable' (ECC1 c f)’
• Relevant bindings include
foldMap' :: (a > m) > ECC1 c f a > m (bound at Bug.hs:18:3)

18  foldMap' f (ECC1 x) = foldMap' f x
 ^^^^^^^^^^^^
```
I would have expected the `(forall p. c p => Foldable' f)` quantified constraint to kick in there.
<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 use forall'd variable in context","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This fails to typecheck, to my surprise:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC1 :: (Type > Constraint) > (Type > Type) > Type > Type where\r\n ECC1 :: c p => f p > ECC1 c f p\r\n\r\nclass Foldable' f where\r\n foldMap' :: Monoid m => (a > m) > f a > m\r\n\r\ninstance (forall p. c p => Foldable' f) => Foldable' (ECC1 c f) where\r\n foldMap' f (ECC1 x) = foldMap' f x\r\n\r\ninstance Foldable' [] where\r\n foldMap' = foldMap\r\n\r\ntest :: ECC1 Show [] Ordering > Ordering\r\ntest = foldMap' id\r\n}}}\r\n\r\n{{{\r\n$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:18:25: error:\r\n • Could not deduce: c p0 arising from a use of ‘foldMap'’\r\n from the context: forall p. c p => Foldable' f\r\n bound by the instance declaration at Bug.hs:17:1063\r\n or from: Monoid m\r\n bound by the type signature for:\r\n foldMap' :: forall m a. Monoid m => (a > m) > ECC1 c f a > m\r\n at Bug.hs:18:310\r\n or from: c a\r\n bound by a pattern with constructor:\r\n ECC1 :: forall (f :: * > *) p (c :: * > Constraint).\r\n c p =>\r\n f p > ECC1 c f p,\r\n in an equation for ‘foldMap'’\r\n at Bug.hs:18:1520\r\n • In the expression: foldMap' f x\r\n In an equation for ‘foldMap'’: foldMap' f (ECC1 x) = foldMap' f x\r\n In the instance declaration for ‘Foldable' (ECC1 c f)’\r\n • Relevant bindings include\r\n foldMap' :: (a > m) > ECC1 c f a > m (bound at Bug.hs:18:3)\r\n \r\n18  foldMap' f (ECC1 x) = foldMap' f x\r\n  ^^^^^^^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall p. c p => Foldable' f)` quantified constraint to kick in there.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14860QuantifiedConstraints: Can't quantify constraint involving type family20200207T14:09:10ZRyan ScottQuantifiedConstraints: Can't quantify constraint involving type familyThis program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE Undecidabl...This program fails to typecheck using the `wip/T2893` branch, to my surprise:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Proxy
type family Apply (f :: * > *) a
type instance Apply Proxy a = Proxy a
data ExTyFam f where
MkExTyFam :: Apply f a > ExTyFam f
instance (forall a. Show (Apply f a)) => Show (ExTyFam f) where
show (MkExTyFam x) = show x
showsPrec = undefined  Not defining these leads to the oddities observed in
showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32
test :: ExTyFam Proxy > String
test = show
```
This fails with:
```
$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:24: error:
• Could not deduce (Show (Apply f a)) arising from a use of ‘show’
from the context: forall a. Show (Apply f a)
bound by the instance declaration at Bug.hs:16:1057
• In the expression: show x
In an equation for ‘show’: show (MkExTyFam x) = show x
In the instance declaration for ‘Show (ExTyFam f)’

17  show (MkExTyFam x) = show x
 ^^^^^^
```
I would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.
<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 quantify constraint involving type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["QuantifiedConstraints","wipT2893"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program fails to typecheck using the `wip/T2893` branch, to my surprise:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE QuantifiedConstraints #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\ntype family Apply (f :: * > *) a\r\ntype instance Apply Proxy a = Proxy a\r\n\r\ndata ExTyFam f where\r\n MkExTyFam :: Apply f a > ExTyFam f\r\n\r\ninstance (forall a. Show (Apply f a)) => Show (ExTyFam f) where\r\n show (MkExTyFam x) = show x\r\n showsPrec = undefined  Not defining these leads to the oddities observed in\r\n showList = undefined  https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32\r\n\r\ntest :: ExTyFam Proxy > String\r\ntest = show\r\n}}}\r\n\r\nThis fails with:\r\n\r\n{{{\r\n$ ghccq/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:17:24: error:\r\n • Could not deduce (Show (Apply f a)) arising from a use of ‘show’\r\n from the context: forall a. Show (Apply f a)\r\n bound by the instance declaration at Bug.hs:16:1057\r\n • In the expression: show x\r\n In an equation for ‘show’: show (MkExTyFam x) = show x\r\n In the instance declaration for ‘Show (ExTyFam f)’\r\n \r\n17  show (MkExTyFam x) = show x\r\n  ^^^^^^\r\n}}}\r\n\r\nI would have expected the `(forall a. Show (Apply f a))` quantified constraint to kick in, but it didn't.","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: ‘...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/14808GHC HEAD regression: GADT constructors no longer quantify tyvars in topologic...20190707T18:15:30ZRyan ScottGHC HEAD regression: GADT constructors no longer quantify tyvars in topological orderOriginally noticed in #14796. This program:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a > ECC ctx f a
f...Originally noticed in #14796. This program:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a > ECC ctx f a
f :: [()] > ECC () [] ()
f = ECC @() @[] @()
```
Typechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:5: error:
• Couldn't match type ‘()’ with ‘[]’
Expected type: [()] > ECC (() :: Constraint) [] ()
Actual type: () [] > ECC (() :: Constraint) () []
• In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()

12  f = ECC @() @[] @()
 ^^^^^^^^^^^^^^^
Bug.hs:12:10: error:
• Expected kind ‘* > *’, but ‘()’ has kind ‘*’
• In the type ‘()’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()

12  f = ECC @() @[] @()
 ^^
Bug.hs:12:14: error:
• Expecting one more argument to ‘[]’
Expected a type, but ‘[]’ has kind ‘* > *’
• In the type ‘[]’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()

12  f = ECC @() @[] @()
 ^^
```
This is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs XTypeApplications fprintexplicitforalls
GHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (ctx :: Constraint) (f :: * > *) a.
ctx =>
f a > ECC ctx f a
```
In GHC HEAD, however, it's:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls
GHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (f :: * > *) a (ctx :: Constraint).
ctx =>
f a > ECC ctx f a
```
This regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  simonpj 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"Originally noticed in #14796. This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC ctx f a where\r\n ECC :: ctx => f a > ECC ctx f a\r\n\r\nf :: [()] > ECC () [] ()\r\nf = ECC @() @[] @()\r\n}}}\r\n\r\nTypechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:5: error:\r\n • Couldn't match type ‘()’ with ‘[]’\r\n Expected type: [()] > ECC (() :: Constraint) [] ()\r\n Actual type: () [] > ECC (() :: Constraint) () []\r\n • In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^^^^^^^^^^^^^^\r\n\r\nBug.hs:12:10: error:\r\n • Expected kind ‘* > *’, but ‘()’ has kind ‘*’\r\n • In the type ‘()’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n\r\nBug.hs:12:14: error:\r\n • Expecting one more argument to ‘[]’\r\n Expected a type, but ‘[]’ has kind ‘* > *’\r\n • In the type ‘[]’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n}}}\r\n\r\nThis is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (ctx :: Constraint) (f :: * > *) a.\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nIn GHC HEAD, however, it's:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (f :: * > *) a (ctx :: Constraint).\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nThis regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14795Data type return kinds don't obey the forallornothing rule20190707T18:15:32ZRyan ScottData type return kinds don't obey the forallornothing ruleOriginally noticed [here](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974). GHC accepts this:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Kind
data Fo...Originally noticed [here](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974). GHC accepts this:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Kind
data Foo :: forall a. a > b > Type where
MkFoo :: a > Foo a b
```
Despite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.
The users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [inconsistent design](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215), so I'm opening this ticket to track this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data type return kinds don't obey the forallornothing rule","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally noticed [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974 here]. GHC accepts this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo :: forall a. a > b > Type where\r\n MkFoo :: a > Foo a b\r\n}}}\r\n\r\nDespite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.\r\n\r\nThe users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215 inconsistent design], so I'm opening this ticket to track this.","type_of_failure":"OtherFailure","blocking":[]} >https://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...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/14771TypeError reported too eagerly20210817T15:46:59ZSylvain HenryTypeError reported too eagerlyConsider the following example:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE UndecidableInstances #}
impor...Consider the following example:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE UndecidableInstances #}
import GHC.TypeLits
import Data.Proxy
data DUMMY
type family If c t e where
If True t e = t
If False t e = e
type family F (n :: Nat) where
F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
F n = If (n <=? 8) Int DUMMY
test :: (F n ~ Word) => Proxy n > Int
test _ = 2
test2 :: Proxy (n :: Nat) > Int
test2 p = test p
main :: IO ()
main = do
print (test2 (Proxy :: Proxy 5))
```
The type error is useful:
```
Bug.hs:26:11: error:
• Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
• Relevant bindings include
p :: Proxy n (bound at Bug.hs:26:7)
test2 :: Proxy n > Int (bound at Bug.hs:26:1)

26  test2 p = test p
 ^^^^^^
```
Now if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:
```
Bug.hs:26:11: error:
• ERROR
• In the expression: test p
In an equation for ‘test2’: test2 p = test p

26  test2 p = test p
 ^^^^^^
```
While with GHC 8.0.1 we get:
```
/home/hsyl20/tmp/Bug.hs:29:11: error:
• Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
```
1) Could we restore the behavior of GHC 8.0.1?
2) In my real code, when I use DUMMY I get:
```
• Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
Expected type: Word
Actual type: F n
```
If we could get the same report (mentioning the "Actual type") when we use `TypeError` that would be great.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeError reported too eagerly","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":"Bug","description":"Consider the following example:\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE UndecidableInstances #}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\ndata DUMMY\r\n\r\ntype family If c t e where\r\n If True t e = t\r\n If False t e = e\r\n\r\n\r\ntype family F (n :: Nat) where\r\n F n = If (n <=? 8) Int (TypeError (Text \"ERROR\"))\r\n F n = If (n <=? 8) Int DUMMY\r\n\r\ntest :: (F n ~ Word) => Proxy n > Int\r\ntest _ = 2\r\n\r\ntest2 :: Proxy (n :: Nat) > Int\r\ntest2 p = test p\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (test2 (Proxy :: Proxy 5))\r\n}}}\r\n\r\nThe type error is useful:\r\n{{{\r\nBug.hs:26:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n • Relevant bindings include\r\n p :: Proxy n (bound at Bug.hs:26:7)\r\n test2 :: Proxy n > Int (bound at Bug.hs:26:1)\r\n \r\n26  test2 p = test p\r\n  ^^^^^^\r\n}}}\r\n\r\nNow if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:\r\n{{{\r\nBug.hs:26:11: error:\r\n • ERROR\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n \r\n26  test2 p = test p\r\n  ^^^^^^\r\n}}}\r\n\r\nWhile with GHC 8.0.1 we get:\r\n{{{\r\n/home/hsyl20/tmp/Bug.hs:29:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’\r\n with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n}}}\r\n\r\n1) Could we restore the behavior of GHC 8.0.1?\r\n\r\n2) In my real code, when I use DUMMY I get:\r\n{{{\r\n • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’\r\n Expected type: Word\r\n Actual type: F n\r\n}}}\r\nIf we could get the same report (mentioning the \"Actual type\") when we use `TypeError` that would be great.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14766Holey partial type signatures greatly slow down compile times20210409T08:06:14ZAlec TheriaultHoley partial type signatures greatly slow down compile timesThis time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment362957245) into a one file...This time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment362957245) into a one file test case. `Sigs.hs` is exactly like `NoSigs.hs`, except for the fact that it has a bunch of extra type signatures that have a lot of holes. On my machine, this is what compilation times are (I gave up timing after 15 minutes):
<table><tr><td> GHC version </td>
<td> 8.0.2 </td>
<td> 8.2.1 </td>
<td> 8.4.1 (445554b6d9a2263f969e25bb9f532dd0c3a9dc8c) </td></tr>
<tr><td> `NoSigs.hs` </td>
<td> 24.13s </td>
<td> 22.93s </td>
<td> 34.05s </td></tr>
<tr><td> `Sigs.hs` </td>
<td> \>15m </td>
<td> \~13m </td>
<td> \>15m </td></tr></table>https://gitlab.haskell.org/ghc/ghc//issues/14763GHC 8.4.1alpha regression with FunctionalDependencies20190707T18:15:43ZRyan ScottGHC 8.4.1alpha regression with FunctionalDependenciesThis regression prevents `esqueleto2.5.3` from building with GHC 8.4.1. Here is a minimized example of the problem:
```hs
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE Multi...This regression prevents `esqueleto2.5.3` from building with GHC 8.4.1. Here is a minimized example of the problem:
```hs
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
data Value a = Value a
data SomeValue expr where
SomeValue :: Esqueleto query expr backend => expr (Value a) > SomeValue expr
class Esqueleto (query :: * > *) (expr :: * > *) backend
 query > expr backend, expr > query backend
data SqlQuery a
data SqlBackend
data SqlExpr a where
ECompositeKey :: SqlExpr (Value a)
instance Esqueleto SqlQuery SqlExpr SqlBackend
match' :: SomeValue SqlExpr > a
match' (SomeValue ECompositeKey) = undefined
```
On GHC 8.2.2, this typechecks without issue. On GHC 8.4.1alpha (version 8.4.0.20180204), this fails with:
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180204: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:25:19: error:
• Could not deduce: query ~ SqlQuery
arising from a functional dependency between:
constraint ‘Esqueleto query SqlExpr backend’
arising from a pattern with constructor:
SomeValue :: forall (query :: * > *) (expr :: * > *) backend a.
Esqueleto query expr backend =>
expr (Value a) > SomeValue expr,
in an equation for ‘match'’
instance ‘Esqueleto SqlQuery SqlExpr SqlBackend’ at Bug.hs:22:1046
from the context: Value a1 ~ Value a2
bound by a pattern with constructor:
ECompositeKey :: forall a. SqlExpr (Value a),
in an equation for ‘match'’
at Bug.hs:25:1931
‘query’ is a rigid type variable bound by
a pattern with constructor:
SomeValue :: forall (query :: * > *) (expr :: * > *) backend a.
Esqueleto query expr backend =>
expr (Value a) > SomeValue expr,
in an equation for ‘match'’
at Bug.hs:25:931
Inaccessible code in
a pattern with constructor:
ECompositeKey :: forall a. SqlExpr (Value a),
in an equation for ‘match'’
• In the pattern: ECompositeKey
In the pattern: SomeValue ECompositeKey
In an equation for ‘match'’:
match' (SomeValue ECompositeKey) = undefined

25  match' (SomeValue ECompositeKey) = undefined
 ^^^^^^^^^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14747DisambiguateRecordFields fails for PatternSynonyms20190707T18:15:46ZAdam GundryDisambiguateRecordFields fails for PatternSynonymsConsider:
```hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern S{x} = [x]
```
```hs
{# LANGUAGE PatternSynonyms, DisambiguateRecordFields #}
module B where
import A
pattern T{x} = [x]
e = S { x = 42 }
```
Compiling mo...Consider:
```hs
{# LANGUAGE PatternSynonyms #}
module A where
pattern S{x} = [x]
```
```hs
{# LANGUAGE PatternSynonyms, DisambiguateRecordFields #}
module B where
import A
pattern T{x} = [x]
e = S { x = 42 }
```
Compiling module B fails with `Ambiguous occurrence ‘x’` in the definition of `e`. In principle, `DisambiguateRecordFields` should select the field belonging to the `S` "data constructor". However, the current implementation of this works by identifying the parent type constructor, which doesn't exist for a pattern synonym.
This continues to fail if `T` is replaced by a data type with a field `x`. If `S` is replaced by a data type, however, it starts working.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #11283 
 Blocking  
 CC  mpickering 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"DisambiguateRecordFields fails for PatternSynonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[11283],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":["mpickering"],"type":"Bug","description":"Consider:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms #}\r\n\r\nmodule A where\r\n\r\npattern S{x} = [x]\r\n}}}\r\n\r\n{{{#!hs\r\n{# LANGUAGE PatternSynonyms, DisambiguateRecordFields #}\r\n\r\nmodule B where\r\n\r\nimport A\r\n\r\npattern T{x} = [x]\r\n\r\ne = S { x = 42 }\r\n}}}\r\n\r\nCompiling module B fails with `Ambiguous occurrence ‘x’` in the definition of `e`. In principle, `DisambiguateRecordFields` should select the field belonging to the `S` \"data constructor\". However, the current implementation of this works by identifying the parent type constructor, which doesn't exist for a pattern synonym.\r\n\r\nThis continues to fail if `T` is replaced by a data type with a field `x`. If `S` is replaced by a data type, however, it starts working.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Adam GundryAdam Gundryhttps://gitlab.haskell.org/ghc/ghc//issues/14728Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?20190707T18:15:51ZRyan ScottIs (GeneralizedNewtypeDeriving + associated type classes) completely bogus?In [D2636](https://phabricator.haskell.org/D2636), I implemented this ability to use `GeneralizedNewtypeDeriving` to derive instances of type classes with associated type families. At the time, I thought the implementation was a nobrain...In [D2636](https://phabricator.haskell.org/D2636), I implemented this ability to use `GeneralizedNewtypeDeriving` to derive instances of type classes with associated type families. At the time, I thought the implementation was a nobrainer, but now I'm starting to have second thoughts. To explain what I mean, consider this program:
```hs
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Functor.Identity
import Data.Kind
class C (a :: Type) where
type T a (x :: a) :: Type
instance C () where
type T () '() = Bool
deriving instance C (Identity a)
```
Quite to my surprise, this typechecks. Let's consult `ddumpderiv` to figure out what code is being generated:
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs ddumpderiv
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance Bug.C (Data.Functor.Identity.Identity a) where
Derived type family instances:
type Bug.T (Data.Functor.Identity.Identity a1_a1M3) x_a1M5 = Bug.T
a1_a1M3 x_a1M5
```
Hm... OK. Since GHC was able to generate this code, surely we should be able to write it ourselves, right?
```hs
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Functor.Identity
import Data.Kind
class C (a :: Type) where
type T a (x :: a) :: Type
instance C () where
type T () '() = Bool
 deriving instance C (Identity a)
instance C (Identity a) where
type T (Identity a) x = T a x
```
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:19:31: error:
• Occurs check: cannot construct the infinite kind: a ~ Identity a
• In the second argument of ‘T’, namely ‘x’
In the type ‘T a x’
In the type instance declaration for ‘T’

19  type T (Identity a) x = T a x
 ^
```
Uhoh. GHC gets quite angry when we try to type this in ourselves, which isn't a good sign. This raises the question: just what is GHC doing in the previous version of the program? I tried to answer that question by seeing if `T (Identity a) x` could ever reduce:
```hs
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE StandaloneDeriving #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Functor.Identity
import Data.Kind
class C (a :: Type) where
type T a (x :: a) :: Type
instance C () where
type T () '() = Bool
deriving instance C (Identity a)
f :: T (Identity ()) ('Identity '())
f = True
```
And lo and behold, you get:
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:19:5: error:
• Couldn't match type ‘T () ('Identity '())’ with ‘Bool’
Expected type: T (Identity ()) ('Identity '())
Actual type: Bool
• In the expression: True
In an equation for ‘f’: f = True

19  f = True
 ^^^^
```
It appears that `T (Identity ()) ('Identity '())` reduced to `T () ('Identity '())`. At that point, it becomes stuck. (Perhaps it's for the best that it's the case—if `T () ('Identity '())` managed to reduce, who knows what kind of mischief GHC could get itself into.)
But all of this leads me to wonder: is something broken in the implementation of this feature, or is `GeneralizedNewtypeDeriving` simply not sound with respect to associated type families? I certainly hope that it's not the latter, as it's quite a useful feature. But at the same time, it's hard to reconcile that usefulness with the strange behavior above.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies","deriving,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In Phab:D2636, I implemented this ability to use `GeneralizedNewtypeDeriving` to derive instances of type classes with associated type families. At the time, I thought the implementation was a nobrainer, but now I'm starting to have second thoughts. To explain what I mean, consider this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Functor.Identity\r\nimport Data.Kind\r\n\r\nclass C (a :: Type) where\r\n type T a (x :: a) :: Type\r\n\r\ninstance C () where\r\n type T () '() = Bool\r\n\r\nderiving instance C (Identity a)\r\n}}}\r\n\r\nQuite to my surprise, this typechecks. Let's consult `ddumpderiv` to figure out what code is being generated:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs ddumpderiv\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance Bug.C (Data.Functor.Identity.Identity a) where\r\n \r\n\r\nDerived type family instances:\r\n type Bug.T (Data.Functor.Identity.Identity a1_a1M3) x_a1M5 = Bug.T\r\n a1_a1M3 x_a1M5\r\n}}}\r\n\r\nHm... OK. Since GHC was able to generate this code, surely we should be able to write it ourselves, right?\r\n\r\n{{{#!hs\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Functor.Identity\r\nimport Data.Kind\r\n\r\nclass C (a :: Type) where\r\n type T a (x :: a) :: Type\r\n\r\ninstance C () where\r\n type T () '() = Bool\r\n\r\n deriving instance C (Identity a)\r\n\r\ninstance C (Identity a) where\r\n type T (Identity a) x = T a x\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:19:31: error:\r\n • Occurs check: cannot construct the infinite kind: a ~ Identity a\r\n • In the second argument of ‘T’, namely ‘x’\r\n In the type ‘T a x’\r\n In the type instance declaration for ‘T’\r\n \r\n19  type T (Identity a) x = T a x\r\n  ^\r\n}}}\r\n\r\nUhoh. GHC gets quite angry when we try to type this in ourselves, which isn't a good sign. This raises the question: just what is GHC doing in the previous version of the program? I tried to answer that question by seeing if `T (Identity a) x` could ever reduce:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE StandaloneDeriving #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Functor.Identity\r\nimport Data.Kind\r\n\r\nclass C (a :: Type) where\r\n type T a (x :: a) :: Type\r\n\r\ninstance C () where\r\n type T () '() = Bool\r\n\r\nderiving instance C (Identity a)\r\n\r\nf :: T (Identity ()) ('Identity '())\r\nf = True\r\n}}}\r\n\r\nAnd lo and behold, you get:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:19:5: error:\r\n • Couldn't match type ‘T () ('Identity '())’ with ‘Bool’\r\n Expected type: T (Identity ()) ('Identity '())\r\n Actual type: Bool\r\n • In the expression: True\r\n In an equation for ‘f’: f = True\r\n \r\n19  f = True\r\n  ^^^^\r\n}}}\r\n\r\nIt appears that `T (Identity ()) ('Identity '())` reduced to `T () ('Identity '())`. At that point, it becomes stuck. (Perhaps it's for the best that it's the case—if `T () ('Identity '())` managed to reduce, who knows what kind of mischief GHC could get itself into.)\r\n\r\nBut all of this leads me to wonder: is something broken in the implementation of this feature, or is `GeneralizedNewtypeDeriving` simply not sound with respect to associated type families? I certainly hope that it's not the latter, as it's quite a useful feature. But at the same time, it's hard to reconcile that usefulness with the strange behavior above.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14723GHC 8.4.1alpha loops infinitely when typechecking20190707T18:15:52ZRyan ScottGHC 8.4.1alpha loops infinitely when typecheckingThis issue prevents `jvmstreaming` from compiling with GHC 8.4.1alpha2. Here is my best attempt at minimizing the issue:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE KindSignatures #}
{# LANG...This issue prevents `jvmstreaming` from compiling with GHC 8.4.1alpha2. Here is my best attempt at minimizing the issue:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FunctionalDependencies #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
module Bug () where
import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import Data.String (fromString)
import Data.Int (Int64)
import GHC.Stack (HasCallStack)
import GHC.TypeLits (Nat, Symbol)
data JType = Iface Symbol
data J (a :: JType)
newIterator
:: IO (J ('Iface "java.util.Iterator"))
newIterator = do
let tblPtr :: Int64
tblPtr = undefined
iterator <
(loadJavaWrappers >>
(((((((qqMarker
(Proxy ::
Proxy "{ return new java.util.Iterator() {\n @Override\n public native boolean hasNext();\n\n @Override\n public native Object next();\n\n @Override\n public void remove() {\n throw new UnsupportedOperationException();\n }\n\n private native void hsFinalize(long tblPtr);\n\n @Override\n public void finalize() {\n hsFinalize($tblPtr);\n }\n } ; }"))
(Proxy :: Proxy "inline__method_0"))
(Proxy :: Proxy "tblPtr"))
(Proxy :: Proxy 106))
(tblPtr, ()))
Proxy)
(((callStatic
(fromString
"io.tweag.inlinejava.Inline__jvmstreaming022inplace_Language_Java_Streaming"))
(fromString "inline__method_0"))
[coerce tblPtr])))
undefined
class Coercible (a :: Type) where
type Ty a :: JType
class Coercibles xs (tys :: k)  xs > tys
instance Coercibles () ()
instance (ty ~ Ty x, Coercible x, Coercibles xs tys) => Coercibles (x, xs) '(ty, tys)
qqMarker
:: forall
 k  the kind variable shows up in Core
(args_tys :: k)  JType's of arguments
tyres  JType of result
(input :: Symbol)  input string of the quasiquoter
(mname :: Symbol)  name of the method to generate
(antiqs :: Symbol)  antiquoted variables as a commaseparated list
(line :: Nat)  line number of the quasiquotation
args_tuple  uncoerced argument types
b.  uncoerced result type
(tyres ~ Ty b, Coercibles args_tuple args_tys, Coercible b, HasCallStack)
=> Proxy input
> Proxy mname
> Proxy antiqs
> Proxy line
> args_tuple
> Proxy args_tys
> IO b
> IO b
qqMarker = undefined
```
With GHC 8.2.2, this is properly rejected by the typechecker:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:27:12: error:
Variable not in scope: loadJavaWrappers :: IO a0

27  (loadJavaWrappers >>
 ^^^^^^^^^^^^^^^^
Bug.hs:36:16: error:
Variable not in scope: callStatic :: t0 > t1 > [a2] > IO a1

36  (((callStatic
 ^^^^^^^^^^
Bug.hs:40:17: error: Variable not in scope: coerce :: Int64 > a2

40  [coerce tblPtr])))
 ^^^^^^
```
But in GHC 8.4.1alpha2, this simply hangs forever.
To make things more interesting, if you pass `ddumptctrace` when compiling, you'll get a panic:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs ddumptctrace
...
kcLHsQTyVars: cusk
JType
[]
[]
[]
[]
*
[]
[]
[]
[]
kcTyClGroup: initial kinds
[rB8 :> ATcTyCon JType :: *, rB9 :> APromotionErr RecDataConPE]
txExtendKindEnv
[rB8 :> ATcTyCon JType :: *, rB9 :> APromotionErr RecDataConPE]
kcTyClDecl { JType
env2 []
tcExtendBinderStack []
env2 []
tcExtendBinderStack []
lk1 Symbol
tcTyVar2a
Symbol
*
u_tys
tclvl 1
* ~ TYPE t_a1qq[tau:1]
arising from a type equality * ~ TYPE t_a1qq[tau:1]
u_tys
tclvl 1
'GHC.Types.LiftedRep ~ t_a1qq[tau:1]
arising from a type equality * ~ TYPE t_a1qq[tau:1]
u_tys
tclvl 1
GHC.Types.RuntimeRep ~ GHC.Types.RuntimeRep
arising from a kind equality arising from
t_a1qq[tau:1] ~ 'GHC.Types.LiftedRep
u_tys yields no coercion
writeMetaTyVar
t_a1qq[tau:1] :: GHC.Types.RuntimeRep := 'GHC.Types.LiftedRep
u_tys yields no coercion
u_tys yields no coercion
checkExpectedKind
*
TYPE t_a1qq[tau:1]
<*>_N
kcLHsQTyVars: notcuskghc: panic! (the 'impossible' happened)
(GHC version 8.4.0.20180118 for x86_64unknownlinux):
kcConDecl
```8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14720GHC 8.4.1alpha regression with TypeInType20190707T18:15:53ZRyan ScottGHC 8.4.1alpha regression with TypeInTypeGHC 8.2.2 is able to typecheck this code:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE Ty...GHC 8.2.2 is able to typecheck this code:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
class Generic (a :: Type) where
type Rep a :: Type
from :: a > Rep a
to :: Rep a > a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a > Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a
data Decision a = Proved a
 Disproved (a > Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
=> Sing a > Sing b > Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) >
case (sTof s1, sTof s2) of
(Refl, Refl) > Proved Refl
Disproved contra > Disproved (\Refl > contra Refl)
```
But GHC 8.4.1alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:3740
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a noninjective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl > contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a > Sing b > Decision (a :~: b)
(bound at Bug.hs:40:3)

44  Disproved contra > Disproved (\Refl > contra Refl)
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a > Rep a\r\n to :: Rep a > a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a > Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)\r\n\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\r\n sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a\r\n\r\ndata Decision a = Proved a\r\n  Disproved (a > Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))\r\n => Sing a > Sing b > Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) >\r\n case (sTof s1, sTof s2) of\r\n (Refl, Refl) > Proved Refl\r\n Disproved contra > Disproved (\\Refl > contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:3740\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a noninjective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl > contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a > Sing b > Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n \r\n44  Disproved contra > Disproved (\\Refl > contra Refl)\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14715GHC 8.4.1alpha regression with PartialTypeSignatures20190707T18:15:54ZRyan ScottGHC 8.4.1alpha regression with PartialTypeSignaturesThis bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE Parti...This bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:
```hs
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# OPTIONS_GHC Wnopartialtypesignatures #}
module Bug (bench_mulPublic) where
data Cyc r
data CT zp r'q
class Reduce a b
type family LiftOf b
bench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)
bench_mulPublic pt sk = do
ct :: CT zp (Cyc zq) < encrypt sk pt
undefined ct
encrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))
encrypt = undefined
```
On GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: error:
• Could not deduce (Reduce fsk0 zq)
from the context: (z ~ LiftOf zq, Reduce fsk zq)
bound by the inferred type for ‘bench_mulPublic’:
forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)
at Bug.hs:(15,1)(17,14)
The type variable ‘fsk0’ is ambiguous
• In the ambiguity check for the inferred type for ‘bench_mulPublic’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
bench_mulPublic :: forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp > Cyc z > IO (zp, zq)

15  bench_mulPublic pt sk = do
 ^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug prevents `lolapps`' tests and benchmarks from building with GHC 8.4.1alpha2. This is as much as I'm able to minimize the issue:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE PartialTypeSignatures #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# OPTIONS_GHC Wnopartialtypesignatures #}\r\nmodule Bug (bench_mulPublic) where\r\n\r\ndata Cyc r\r\ndata CT zp r'q\r\nclass Reduce a b\r\ntype family LiftOf b\r\n\r\nbench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp > Cyc z > IO (zp,zq)\r\nbench_mulPublic pt sk = do\r\n ct :: CT zp (Cyc zq) < encrypt sk pt\r\n undefined ct\r\n\r\nencrypt :: forall z zp zq. Reduce z zq => Cyc z > Cyc zp > IO (CT zp (Cyc zq))\r\nencrypt = undefined\r\n}}}\r\n\r\nOn GHC 8.2.2, this compiles without issue. But on GHC 8.4.1alpha2, this errors with:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: error:\r\n • Could not deduce (Reduce fsk0 zq)\r\n from the context: (z ~ LiftOf zq, Reduce fsk zq)\r\n bound by the inferred type for ‘bench_mulPublic’:\r\n forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n at Bug.hs:(15,1)(17,14)\r\n The type variable ‘fsk0’ is ambiguous\r\n • In the ambiguity check for the inferred type for ‘bench_mulPublic’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the inferred type\r\n bench_mulPublic :: forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp > Cyc z > IO (zp, zq)\r\n \r\n15  bench_mulPublic pt sk = do\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14710GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds20190707T18:15:55ZRyan ScottGHC 8.4.1alpha allows the use of kind polymorphism without PolyKindsThis program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGU...This program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# OPTIONS_GHC ddumpderiv #}
module Bug where
import Data.Coerce
import Data.Proxy
class C a b where
c :: Proxy (x :: a) > b
newtype I a = MkI a
instance C x a => C x (Bug.I a) where
c = coerce @(forall (z :: x). Proxy z > a)
@(forall (z :: x). Proxy z > I a)
c
```
is rightfully rejected by GHC 8.2.2:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

20  c = coerce @(forall (z :: x). Proxy z > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:21:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

21  @(forall (z :: x). Proxy z > I a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But GHC 8.4.1alpha2 actually //accepts// this program!
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
```
This is almost certainly bogus.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug where\r\n\r\nimport Data.Coerce\r\nimport Data.Proxy\r\n\r\nclass C a b where\r\n c :: Proxy (x :: a) > b\r\n\r\nnewtype I a = MkI a\r\n\r\ninstance C x a => C x (Bug.I a) where\r\n c = coerce @(forall (z :: x). Proxy z > a)\r\n @(forall (z :: x). Proxy z > I a)\r\n c\r\n}}}\r\n\r\nis rightfully rejected by GHC 8.2.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n20  c = coerce @(forall (z :: x). Proxy z > a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:21:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n21  @(forall (z :: x). Proxy z > I a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 actually //accepts// this program!\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs\r\nGHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\n}}}\r\n\r\nThis is almost certainly bogus.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14693Computing imp_finst can take up significant amount of time20190707T18:15:59ZniteriaComputing imp_finst can take up significant amount of timeI profiled a build of a production code base with thousands of modules and merging `imp_finsts` \[1\] from different imports came up on top taking up 9% of total compile time.
I made a synthetic test case to reproduce the issue (see att...I profiled a build of a production code base with thousands of modules and merging `imp_finsts` \[1\] from different imports came up on top taking up 9% of total compile time.
I made a synthetic test case to reproduce the issue (see attached `generateModules`).
The test case is basically multiple layers of modules where each module defines a type family instance through deriving Generic.
The problem is quite obvious, `unionLists` is quadratic and `imp_finsts` just keeps growing with the size of the code base.
\[1\] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/typecheck/TcRnTypes.hs;575c009d9e4b25384ef984c09b2c54f909693e93$1398
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 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":"Computing imp_finst can take up significant amount of time","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I profiled a build of a production code base with thousands of modules and merging `imp_finsts` [1] from different imports came up on top taking up 9% of total compile time.\r\n\r\nI made a synthetic test case to reproduce the issue (see attached `generateModules`).\r\nThe test case is basically multiple layers of modules where each module defines a type family instance through deriving Generic.\r\n\r\nThe problem is quite obvious, `unionLists` is quadratic and `imp_finsts` just keeps growing with the size of the code base.\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n[1] https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/typecheck/TcRnTypes.hs;575c009d9e4b25384ef984c09b2c54f909693e93$1398","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14691Replace EvTerm with CoreExpr20190707T18:15:59ZJoachim Breitnermail@joachimbreitner.deReplace EvTerm with CoreExprI asked
> I had some funky idea where a type checker plugin would have to \ synthesize code for a customsolved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)
...I asked
> I had some funky idea where a type checker plugin would have to \ synthesize code for a customsolved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)
>
> What would break if we had
>
> ```
>  EvExpr CoreExpr
> ```
>
> as an additional constructor there?
And Simon said
> This has come up before. I think that'd be a solid win.
>
> In fact, eliminate all the existing evidence constructors with "smart constructors" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.
>
> I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.
>
> You'd need to add `zonkCoreExpr` in place of `zonkEvTerm`.
>
> `evVarsOfTerm` is called quite a bit; you might want to cache the result in the `EvExpr` constructor.
This ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Task 
 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":"Replace EvTerm with CoreExpr","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"I asked\r\n\r\n> I had some funky idea where a type checker plugin would have to  synthesize code for a customsolved instances on the fly. But it seems that does not work because EvTerm is less expressive than Core (especially, no lambdas)\r\n>\r\n> What would break if we had\r\n> {{{\r\n>  EvExpr CoreExpr\r\n> }}}\r\n> as an additional constructor there?\r\n\r\nAnd Simon said\r\n\r\n> This has come up before. I think that'd be a solid win. \r\n> \r\n> In fact, eliminate all the existing evidence constructors with \"smart constructors\" that produce an EvExpr. That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.\r\n> \r\n> I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.\r\n>\r\n> You'd need to add `zonkCoreExpr` in place of `zonkEvTerm`.\r\n>\r\n> `evVarsOfTerm` is called quite a bit; you might want to cache the result in the `EvExpr` constructor.\r\n\r\nThis ticket tracks it. Not sure if i get to it right away, but I am happy to advise, review, and play around with the result.\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14668Ordering of declarations can cause typechecking to fail20210328T19:49:34ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
...The following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14618Higher rank typechecking is broken20190707T18:16:16ZmniipHigher rank typechecking is brokenThe oddity was noticed when someone asked the type of `lens` from lambdabot and it replied with
```hs
1514165211 [04:26:51] <lambdabot> Functor f => (s1 > a1) > (s1 > b1 > t1) > (a2 > f b2) > s2 > f t2
```
This disagrees with `...The oddity was noticed when someone asked the type of `lens` from lambdabot and it replied with
```hs
1514165211 [04:26:51] <lambdabot> Functor f => (s1 > a1) > (s1 > b1 > t1) > (a2 > f b2) > s2 > f t2
```
This disagrees with `lens`'s type per definition (way too many foralls and unconstrained type variables), and if handled carefully it could be used to implement `unsafeCoerce` within SafeHaskell.
The minimalest example I could come up with:
```hs
{# LANGUAGE RankNTypes #}
safeCoerce :: a > b
safeCoerce = f'
where
f :: d > forall c. d
f x = x
f' = f
```
This compiles and typechecks on GHC 8.2.2, 8.2.1 (courtesy of hydraz) and HEAD.
But not on 8.0.2 (hydraz) or 7.10.3.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  hydraz 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Higher rank typechecking is broken","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":["hydraz"],"type":"Bug","description":"The oddity was noticed when someone asked the type of `lens` from lambdabot and it replied with\r\n{{{#!hs\r\n1514165211 [04:26:51] <lambdabot> Functor f => (s1 > a1) > (s1 > b1 > t1) > (a2 > f b2) > s2 > f t2\r\n}}}\r\n\r\nThis disagrees with `lens`'s type per definition (way too many foralls and unconstrained type variables), and if handled carefully it could be used to implement `unsafeCoerce` within SafeHaskell.\r\n\r\nThe minimalest example I could come up with:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n \r\nsafeCoerce :: a > b\r\nsafeCoerce = f'\r\n where\r\n f :: d > forall c. d\r\n f x = x\r\n\r\n f' = f\r\n}}}\r\n\r\nThis compiles and typechecks on GHC 8.2.2, 8.2.1 (courtesy of hydraz) and HEAD.\r\nBut not on 8.0.2 (hydraz) or 7.10.3.","type_of_failure":"OtherFailure","blocking":[]} >8.2.3https://gitlab.haskell.org/ghc/ghc//issues/14579GeneralizedNewtypeDeriving produces ambiguouslykinded code20200628T13:19:49ZRyan ScottGeneralizedNewtypeDeriving produces ambiguouslykinded codeThis program //should// compile:
```hs
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
deriving Eq
n...This program //should// compile:
```hs
{# LANGUAGE GeneralizedNewtypeDeriving #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
newtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)
deriving Eq
newtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))
deriving Eq
```
After all, it //should// produce this `Eq (Glurp a)` instance, which compiles without issue:
```hs
instance Eq a => Eq (Glurp a) where
(==) = coerce @(Wat ('Proxy :: Proxy a) > Wat ('Proxy :: Proxy a) > Bool)
@(Glurp a > Glurp a > Bool)
(==)
```
But despite my wishful thinking, GHC does not actually do this. In fact, the code that GHC tries to generate for an `Eq (Glurp a)` instance is completely wrong:
```
$ /opt/ghc/8.2.2/bin/ghci ddumpderiv Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
==================== Derived instances ====================
Derived class instances:
instance forall a (x :: Data.Proxy.Proxy a).
GHC.Classes.Eq a =>
GHC.Classes.Eq (Bug.Wat x) where
(GHC.Classes.==)
= GHC.Prim.coerce
@(GHC.Base.Maybe a_a2wE > GHC.Base.Maybe a_a2wE > GHC.Types.Bool)
@(Bug.Wat x_a2wF > Bug.Wat x_a2wF > GHC.Types.Bool)
(GHC.Classes.==)
(GHC.Classes./=)
= GHC.Prim.coerce
@(GHC.Base.Maybe a_a2wE > GHC.Base.Maybe a_a2wE > GHC.Types.Bool)
@(Bug.Wat x_a2wF > Bug.Wat x_a2wF > GHC.Types.Bool)
(GHC.Classes./=)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where
(GHC.Classes.==)
= GHC.Prim.coerce
@(Bug.Wat Data.Proxy.Proxy
> Bug.Wat Data.Proxy.Proxy > GHC.Types.Bool)
@(Bug.Glurp a_a1vT > Bug.Glurp a_a1vT > GHC.Types.Bool)
(GHC.Classes.==)
(GHC.Classes./=)
= GHC.Prim.coerce
@(Bug.Wat Data.Proxy.Proxy
> Bug.Wat Data.Proxy.Proxy > GHC.Types.Bool)
@(Bug.Glurp a_a1vT > Bug.Glurp a_a1vT > GHC.Types.Bool)
(GHC.Classes./=)
Derived type family instances:
Bug.hs:12:12: error:
• Couldn't match representation of type ‘a0’ with that of ‘a’
arising from a use of ‘GHC.Prim.coerce’
‘a’ is a rigid type variable bound by
the instance declaration at Bug.hs:12:1213
• In the expression:
GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(==)
In an equation for ‘==’:
(==)
= GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(==)
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Glurp a)’:
To see the code I am typechecking, use ddumpderiv
In the instance declaration for ‘Eq (Glurp a)’
• Relevant bindings include
(==) :: Glurp a > Glurp a > Bool (bound at Bug.hs:12:12)

12  deriving Eq
 ^^
Bug.hs:12:12: error:
• Could not deduce (Eq a0) arising from a use of ‘==’
from the context: Eq a
bound by the instance declaration at Bug.hs:12:1213
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance forall k (s :: k). Eq (Proxy s)  Defined in ‘Data.Proxy’
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’
...plus 25 others
...plus 9 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the third argument of ‘GHC.Prim.coerce’, namely ‘(==)’
In the expression:
GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(==)
In an equation for ‘==’:
(==)
= GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(==)
When typechecking the code for ‘==’
in a derived instance for ‘Eq (Glurp a)’:
To see the code I am typechecking, use ddumpderiv

12  deriving Eq
 ^^
Bug.hs:12:12: error:
• Couldn't match representation of type ‘a1’ with that of ‘a’
arising from a use of ‘GHC.Prim.coerce’
‘a’ is a rigid type variable bound by
the instance declaration at Bug.hs:12:1213
• In the expression:
GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(/=)
In an equation for ‘/=’:
(/=)
= GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(/=)
When typechecking the code for ‘/=’
in a derived instance for ‘Eq (Glurp a)’:
To see the code I am typechecking, use ddumpderiv
In the instance declaration for ‘Eq (Glurp a)’
• Relevant bindings include
(/=) :: Glurp a > Glurp a > Bool (bound at Bug.hs:12:12)

12  deriving Eq
 ^^
Bug.hs:12:12: error:
• Could not deduce (Eq a1) arising from a use of ‘/=’
from the context: Eq a
bound by the instance declaration at Bug.hs:12:1213
The type variable ‘a1’ is ambiguous
These potential instances exist:
instance forall k (s :: k). Eq (Proxy s)  Defined in ‘Data.Proxy’
instance Eq Ordering  Defined in ‘GHC.Classes’
instance Eq Integer
 Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’
...plus 25 others
...plus 9 instances involving outofscope types
(use fprintpotentialinstances to see them all)
• In the third argument of ‘GHC.Prim.coerce’, namely ‘(/=)’
In the expression:
GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(/=)
In an equation for ‘/=’:
(/=)
= GHC.Prim.coerce
@(Wat Proxy > Wat Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(/=)
When typechecking the code for ‘/=’
in a derived instance for ‘Eq (Glurp a)’:
To see the code I am typechecking, use ddumpderiv

12  deriving Eq
 ^^
```
Yikes. To see what went wrong, let's zoom in a particular part of the `ddumpderiv` output (cleaned up a bit for presentation purposes):
```hs
instance Eq a => Eq (Glurp a) where
(==)
= coerce
@(Wat 'Proxy > Wat 'Proxy > Bool)
@(Glurp a > Glurp a > Bool)
(==)
```
Notice that it's `Wat 'Proxy`, and not `Wat ('Proxy :: Proxy a)`! And no, that's not just a result of GHC omitting the kind information—you will see the exact same thing if you compile with `fprintexplicitkinds`. What's going on here?
As it turns out, the types inside of those visible type applications aren't `Type`s, but rather `HsType GhcRn`s (i.e., source syntax). So what is happening is that GHC is literally producing `@(Wat 'Proxy > Wat 'Proxy > Bool)` //as source syntax//, not as a `Type`. This means that `'Proxy` has an underspecified kind, resulting in the numerous `The type variable ‘a0’ is ambiguous` errors you see above.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GeneralizedNewtypeDeriving produces ambiguouslykinded code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["deriving"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program //should// compile:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GeneralizedNewtypeDeriving #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nnewtype Wat (x :: Proxy (a :: Type)) = MkWat (Maybe a)\r\n deriving Eq\r\n\r\nnewtype Glurp a = MkGlurp (Wat ('Proxy :: Proxy a))\r\n deriving Eq\r\n}}}\r\n\r\nAfter all, it //should// produce this `Eq (Glurp a)` instance, which compiles without issue:\r\n\r\n{{{#!hs\r\ninstance Eq a => Eq (Glurp a) where\r\n (==) = coerce @(Wat ('Proxy :: Proxy a) > Wat ('Proxy :: Proxy a) > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n}}}\r\n\r\nBut despite my wishful thinking, GHC does not actually do this. In fact, the code that GHC tries to generate for an `Eq (Glurp a)` instance is completely wrong:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci ddumpderiv Bug.hs\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\n==================== Derived instances ====================\r\nDerived class instances:\r\n instance forall a (x :: Data.Proxy.Proxy a).\r\n GHC.Classes.Eq a =>\r\n GHC.Classes.Eq (Bug.Wat x) where\r\n (GHC.Classes.==)\r\n = GHC.Prim.coerce\r\n @(GHC.Base.Maybe a_a2wE > GHC.Base.Maybe a_a2wE > GHC.Types.Bool)\r\n @(Bug.Wat x_a2wF > Bug.Wat x_a2wF > GHC.Types.Bool)\r\n (GHC.Classes.==)\r\n (GHC.Classes./=)\r\n = GHC.Prim.coerce\r\n @(GHC.Base.Maybe a_a2wE > GHC.Base.Maybe a_a2wE > GHC.Types.Bool)\r\n @(Bug.Wat x_a2wF > Bug.Wat x_a2wF > GHC.Types.Bool)\r\n (GHC.Classes./=)\r\n \r\n instance GHC.Classes.Eq a => GHC.Classes.Eq (Bug.Glurp a) where\r\n (GHC.Classes.==)\r\n = GHC.Prim.coerce\r\n @(Bug.Wat Data.Proxy.Proxy\r\n > Bug.Wat Data.Proxy.Proxy > GHC.Types.Bool)\r\n @(Bug.Glurp a_a1vT > Bug.Glurp a_a1vT > GHC.Types.Bool)\r\n (GHC.Classes.==)\r\n (GHC.Classes./=)\r\n = GHC.Prim.coerce\r\n @(Bug.Wat Data.Proxy.Proxy\r\n > Bug.Wat Data.Proxy.Proxy > GHC.Types.Bool)\r\n @(Bug.Glurp a_a1vT > Bug.Glurp a_a1vT > GHC.Types.Bool)\r\n (GHC.Classes./=)\r\n \r\n\r\nDerived type family instances:\r\n\r\n\r\n\r\nBug.hs:12:12: error:\r\n • Couldn't match representation of type ‘a0’ with that of ‘a’\r\n arising from a use of ‘GHC.Prim.coerce’\r\n ‘a’ is a rigid type variable bound by\r\n the instance declaration at Bug.hs:12:1213\r\n • In the expression:\r\n GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n In an equation for ‘==’:\r\n (==)\r\n = GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n When typechecking the code for ‘==’\r\n in a derived instance for ‘Eq (Glurp a)’:\r\n To see the code I am typechecking, use ddumpderiv\r\n In the instance declaration for ‘Eq (Glurp a)’\r\n • Relevant bindings include\r\n (==) :: Glurp a > Glurp a > Bool (bound at Bug.hs:12:12)\r\n \r\n12  deriving Eq\r\n  ^^\r\n\r\nBug.hs:12:12: error:\r\n • Could not deduce (Eq a0) arising from a use of ‘==’\r\n from the context: Eq a\r\n bound by the instance declaration at Bug.hs:12:1213\r\n The type variable ‘a0’ is ambiguous\r\n These potential instances exist:\r\n instance forall k (s :: k). Eq (Proxy s)  Defined in ‘Data.Proxy’\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’\r\n ...plus 25 others\r\n ...plus 9 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • In the third argument of ‘GHC.Prim.coerce’, namely ‘(==)’\r\n In the expression:\r\n GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n In an equation for ‘==’:\r\n (==)\r\n = GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n When typechecking the code for ‘==’\r\n in a derived instance for ‘Eq (Glurp a)’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n12  deriving Eq\r\n  ^^\r\n\r\nBug.hs:12:12: error:\r\n • Couldn't match representation of type ‘a1’ with that of ‘a’\r\n arising from a use of ‘GHC.Prim.coerce’\r\n ‘a’ is a rigid type variable bound by\r\n the instance declaration at Bug.hs:12:1213\r\n • In the expression:\r\n GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (/=)\r\n In an equation for ‘/=’:\r\n (/=)\r\n = GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (/=)\r\n When typechecking the code for ‘/=’\r\n in a derived instance for ‘Eq (Glurp a)’:\r\n To see the code I am typechecking, use ddumpderiv\r\n In the instance declaration for ‘Eq (Glurp a)’\r\n • Relevant bindings include\r\n (/=) :: Glurp a > Glurp a > Bool (bound at Bug.hs:12:12)\r\n \r\n12  deriving Eq\r\n  ^^\r\n\r\nBug.hs:12:12: error:\r\n • Could not deduce (Eq a1) arising from a use of ‘/=’\r\n from the context: Eq a\r\n bound by the instance declaration at Bug.hs:12:1213\r\n The type variable ‘a1’ is ambiguous\r\n These potential instances exist:\r\n instance forall k (s :: k). Eq (Proxy s)  Defined in ‘Data.Proxy’\r\n instance Eq Ordering  Defined in ‘GHC.Classes’\r\n instance Eq Integer\r\n  Defined in ‘integergmp1.0.1.0:GHC.Integer.Type’\r\n ...plus 25 others\r\n ...plus 9 instances involving outofscope types\r\n (use fprintpotentialinstances to see them all)\r\n • In the third argument of ‘GHC.Prim.coerce’, namely ‘(/=)’\r\n In the expression:\r\n GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (/=)\r\n In an equation for ‘/=’:\r\n (/=)\r\n = GHC.Prim.coerce\r\n @(Wat Proxy > Wat Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (/=)\r\n When typechecking the code for ‘/=’\r\n in a derived instance for ‘Eq (Glurp a)’:\r\n To see the code I am typechecking, use ddumpderiv\r\n \r\n12  deriving Eq\r\n  ^^\r\n}}}\r\n\r\nYikes. To see what went wrong, let's zoom in a particular part of the `ddumpderiv` output (cleaned up a bit for presentation purposes):\r\n\r\n{{{#!hs\r\n instance Eq a => Eq (Glurp a) where\r\n (==)\r\n = coerce\r\n @(Wat 'Proxy > Wat 'Proxy > Bool)\r\n @(Glurp a > Glurp a > Bool)\r\n (==)\r\n}}}\r\n\r\nNotice that it's `Wat 'Proxy`, and not `Wat ('Proxy :: Proxy a)`! And no, that's not just a result of GHC omitting the kind information—you will see the exact same thing if you compile with `fprintexplicitkinds`. What's going on here?\r\n\r\nAs it turns out, the types inside of those visible type applications aren't `Type`s, but rather `HsType GhcRn`s (i.e., source syntax). So what is happening is that GHC is literally producing `@(Wat 'Proxy > Wat 'Proxy > Bool)` //as source syntax//, not as a `Type`. This means that `'Proxy` has an underspecified kind, resulting in the numerous `The type variable ‘a0’ is ambiguous` errors you see above.","type_of_failure":"OtherFailure","blocking":[]} >8.10.1