#14734 closed bug (invalid)
QuantifiedConstraints conflated with impredicative polymorphism?
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
This works:
{-# Language QuantifiedConstraints #-} {-# Language GADTs #-} {-# Language ConstraintKinds #-} {-# Language KindSignatures #-} {-# Language RankNTypes #-} {-# Language FlexibleInstances #-} {-# Language UndecidableInstances #-} {-# Language TypeOperators #-} import Data.Kind data D c where D :: c => D c newtype a :- b = Sub (a => D b) class (forall xx. f xx) => Limit f instance (forall xx. f xx) => Limit f proof :: Limit Eq :- Eq (Int -> Float) proof = Sub D
If we replace Limit Eq
with (forall xx. Eq xx)
it is considered impredicative polymorphism, but is it?
174-quantifiedconstraints.hs:20:10: error: • Illegal polymorphic type: forall xx. Eq xx GHC doesn't yet support impredicative polymorphism • In the type signature: proof :: (forall xx. Eq xx) :- Eq (Int -> Float) | 20 | proof :: (forall xx. Eq xx) :- Eq (Int -> Float) | ^^^^^^^^^^^^^^^^^
Change History (8)
comment:1 Changed 23 months ago by
Keywords: | wipT2893 added |
---|
comment:2 Changed 23 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
comment:3 Changed 22 months ago by
It feels different, there is no way to get around regular impredicativity with type synonyms but in this case we can get around it with the Limit
class synonym.
Hypothetically if GHC were to generate an internal class synonym for impredicative constraints what would go wrong? I'm not aware of differences between forall xx. f xx
and Limit f
.
comment:4 Changed 22 months ago by
It would be nice to directly write type a :- b = Dict (a => b)
rather than
class (a => b) => Implies a b instance (a => b) => Implies a b type a :- b = Dict (Implies a b)
comment:5 Changed 22 months ago by
The difficulty with impredicativity is that, during inference, a unification variable may be unified with a polytype. Thus
f :: forall a. [a] -> [a] xs :: [forall b. b->b] ...(f xs)..
Here f really has a type argument, and that type is polymorphic. We really have
...(f @(forall b b->b) xs)...
The hard bit is infeering the implicit, invisible type arguments.
But here we are the level of types. With explicit arguments there should be nothing wrong with allowing polytypes. (It's a different matter for the implicit kind arguments, of course.)
So... may it'd be OK. I'm just not sure what a principled story is.
comment:7 Changed 21 months ago by
Btw, should the following work?
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Prelude> :set -XGADTs -XQuantifiedConstraints -XConstraintKinds Prelude> data Dict c where Dict :: c => Dict c Prelude> :kind forall a b. Dict (a => b) forall a b. Dict (a => b) :: * Prelude>
comment:8 Changed 18 months ago by
Keywords: | wipT2893 removed |
---|
Yes it is. You are instantiating a type variable (the
a
fromnewtype a :- b
) with a polymorphic type.I think you need impredicativity here.