Higher rank polykinds

2020-05-21 06:24:56

Copy pasting some discussion with @Reed Mullanix from Slack.

It seems like something like the following should work, but it doesn't:

class Composative (t :: forall k. (k -> *) -> k -> *)
  where
  composed :: Compose (t a) (t b) ~> t (Compose a b)

data Compose :: forall x y. (y -> *) -> (x -> y) -> x -> * where
    Compose :: f (g a) -> Compose f g a

instance Monad m => Composative (Compose m)
  where
  composed = _

here's the error:

[typecheck] [E] /mnt/data/depot/git/haskell/experiments/recuest/src/HStructures.hs:35:34: error:
    • Expected kind 'forall k. (k -> *) -> k -> *',
        but 'Compose m' has kind '(k10 -> *) -> k10 -> *'
    • In the first argument of 'Composative', namely '(Compose m)'
      In the instance declaration for 'Composative (Compose m)'

however, as Reed discovered, if you move the quantification in the definition of Compose around, it does:

data Compose (f :: y -> *) :: forall x. (x -> y) -> x -> * where
    Compose :: f (g a) -> Compose f g a

instance Monad m => Composative (Compose m)
  where
  composed = _

Is this an expected limitation? Bug in GHC? Something we're doing wrong?

Asad Saeeduddin

2020-05-21 06:28:21

@Reed Mullanix this works too btw:

data Compose :: forall y. (y -> *) -> forall x. (x -> y) -> x -> *
  where
  Compose :: { getCompose :: f (g a) } -> Compose f g a

TheMatten

2020-05-21 06:34:40

@Asad Saeeduddin does this compile on older versions of GHC?

Asad Saeeduddin

2020-05-21 22:07:12

I don't really know, but I was pointed to the gitlab issue that explains how this is expected behavior: https://gitlab.haskell.org/ghc/ghc/issues/13399

#13399: Location of `forall` matters with higher-rank kind polymorphism · Issues · Glasgow Haskell Compiler / GHC

The following code fails to compile, but probably should: ```hs {-# LANGUAGE RankNTypes, TypeInType #-} import Data.Kind data Foo :: forall k . (* -> *) -> k -> *...

Higher rank polykinds - Haskell