Opened 12 months ago

Closed 12 months ago

Last modified 12 months ago

#15628 closed bug (duplicate)

Higher-rank kinds

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1-beta1
Keywords: ImpredicativeTypes 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

Taken from Data.Eq.Type.Hetero.

(:==) (called HEq to avoid unnecessary extensions) fails if you add a Proxy x -> argument.

{-# Language RankNTypes, KindSignatures, PolyKinds, GADTs, DataKinds #-}

import Data.Kind
import Data.Proxy

newtype HEq :: forall j. j -> forall k. k -> Type where
 HEq
  :: (forall (x::forall xx. xx -> Type). Proxy x -> x a -> x b)
  -> HEq a b
$ ~/code/latestghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 398.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 398.hs, interpreted )

398.hs:7:2: error:
    • A newtype constructor cannot have existential type variables
      HEq :: forall j k xx (a :: j) (b :: k).
             (forall (x :: forall xx1. xx1 -> *). Proxy x -> x a -> x b)
             -> HEq a b
    • In the definition of data constructor ‘HEq’
      In the newtype declaration for ‘HEq’
  |
7 |  HEq
  |  ^^^...
Failed, no modules loaded.
Prelude> 

It compiles fine without Proxy x ->. Now my question is what existential type variable does HEq have, -fprint-explicit-kinds shows that Proxy is actually being instantiated at (xx -> Type) and not (forall xx. xx -> Type)

398.hs:10:2: error:
    • A newtype constructor cannot have existential type variables
      HEq :: forall j k xx (a :: j) (b :: k).
             (forall (x :: forall xx1. xx1 -> *).
              Proxy (xx -> *) (x xx) -> x j a -> x k b)
             -> HEq j a k b
    • In the definition of data constructor ‘HEq’
      In the newtype declaration for ‘HEq’
   |
10 |  HEq
   |  ^^^...

so I suppose my question is, can we instantiate Proxy at a higher-rank kind? (#12045: Proxy @FOO)

>> type FOO = (forall xx. xx -> Type)
>> :kind (Proxy :: FOO -> Type)

<interactive>:1:2: error:
    • Expected kind ‘FOO -> *’, but ‘Proxy’ has kind ‘k0 -> *’
    • In the type ‘(Proxy :: FOO -> Type)’

It is possible to create a bespoke Proxy

type FOO = (forall x. x -> Type)

data BespokeProxy :: FOO -> Type where
  BespokeProxy :: forall (c :: FOO). BespokeProxy c

newtype HEq :: forall j. j -> forall k. k -> Type where
 HEq
  :: (forall (x::forall xx. xx -> Type). BespokeProxy x -> x a -> x b)
  -> HEq a b

Change History (4)

comment:1 Changed 12 months ago by simonpj

Instantiating a polymorphic type variable with a polytype (or polykind) is called "imprediative polymorphism" and is a swamp. GHC just does not have a decent story at the moment. But I think that is what you are asking for.

But see https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/ (PLDI'18).

comment:2 Changed 12 months ago by Iceland_jack

I should have known. I can close it or label it with imprediativity,

I still find it mysterious that

-- works
newtype Bar = Bar (forall (f :: FOO). ())

adding a Proxy induces an existential variable x seemingly without introducing quantification, but this is maybe a problem with my intuition? Or at least something rings odd about this (then again higher-rank kinds are odd and interesting)

-- oops, you are actually writing
--   Proxy @(x -> Type) (f @x)
newtype Bar = Bar (forall (f :: FOO). Proxy f -> ())

comment:3 in reply to:  2 Changed 12 months ago by RyanGlScott

Keywords: ImpredicativeTypes added
Resolution: duplicate
Status: newclosed

Replying to Iceland_jack:

adding a Proxy induces an existential variable x seemingly without introducing quantification

It does introduce quantification, and it's precisely because GHC can't support impredicative polymorphism at the moment. When you write:

newtype Bar = Bar (forall (f :: forall xx. xx -> Type). Proxy f -> ())

Then if we display all arguments visibly, this is what you are trying to write:

newtype Bar = Bar (forall (f :: forall xx. xx -> Type). Proxy @(forall xx. xx -> Type) f -> ())

You can't instantiate Proxy's first argument with forall xx. xx -> Type since it is a polytype, and that would be impredicative. Therefore, GHC has to pick something to instantiate xx with in order to avoid impredicativity. Since we're in a data type, GHC bails out by creating an existentially quantified variable x and using that to instantiate the higher-rank kind:

newtype Bar = forall x. Bar (forall (f :: x -> Type). Proxy @(x -> Type) (f @x) -> ())

But Bar is a newtype, and therefore can't have existentials, leading to your error.

As simonpj notes in comment:1, this ticket is really asking for impredicative polymorphism. There is already a raft of tickets about this topic, so I'll opt to close this one.

comment:4 Changed 12 months ago by goldfire

Just chiming in that I agree with the other analysis. I think GHC is doing the right thing here, given that it can't do impredicative instantiation.

Note: See TracTickets for help on using tickets.