Existentials in newtypes
The following code compiles:
{-# LANGUAGE ConstraintKinds, TypeFamilies, RankNTypes, PolyKinds, KindSignatures #-}
import GHC.Prim
import Data.Proxy
type family Ctx2 ctx a b :: Constraint
newtype Proxy1 c a = P1 (forall b . Ctx2 c a b => Proxy b -> Int)
but if I explicitly poly-kind Ctx2
:
type family Ctx2 ctx a (b :: k) :: Constraint
I get the errors
Main.hs:10:22:
Could not deduce (b ~ b0)
from the context (Ctx2 c a b)
bound by the type of the constructor ‘P1’:
Ctx2 c a b => Proxy b -> Int
at Main.hs:10:22
‘b’ is a rigid type variable bound by
the type of the constructor ‘P1’: Ctx2 c a b => Proxy b -> Int
at Main.hs:10:22
Expected type: Proxy b -> Int
Actual type: Proxy b0 -> Int
In the ambiguity check for the type of the constructor ‘P1’:
P1 :: forall c a (k :: BOX).
(forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘P1’
In the newtype declaration for ‘Proxy1’
Main.hs:10:22:
A newtype constructor cannot have existential type variables
P1 :: forall c a (k :: BOX).
(forall (b :: k). Ctx2 c a b => Proxy b -> Int) -> Proxy1 c a
In the definition of data constructor ‘P1’
In the newtype declaration for ‘Proxy1’
It seems like the code should compile, but I might be missing something. This ticket is really about the second error message: there were existential types in a newtype before and after the change, so this error should occur in both places or neither.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |