PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Simon Peyton-Jones]

Same question.  Do you expect the code below to type-check?  I have stripped it down to essentials.  Currently it’s rejected with

    Couldn't match type `a' with '(,) k k1 b0 d0

And that seems reasonable, doesn’t it?  After all, in the defn of bidStar, (:*) returns a value of type
     Star x y ‘(a,c) ‘(b,d)
which is manifestly incompatible with the claimed, more polymorphic type.  And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason.

I must be confused.

Simon


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)

bidStar :: Star T T a a
bidStar = bidT :* bidT

data T a b = MkT

bidT :: T a a
bidT = MkT

From: Edward Kmett [mailto:ekmett at gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users at haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =(

For instance, there doesn't even seem to be a way to make the following code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type?

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:
With the code below, I get this error message with HEAD. And that looks right to me, no?
The current 7.6 branch gives the same message printed less prettily.

If I replace the defn of irt with
irt :: a '(i,j) -> Thrist a '(i,j)
irt ax = ax :- Nil

then it typechecks.

Simon


Knett.hs:20:10:
    Couldn't match type `x' with '(i0, k0)
      `x' is a rigid type variable bound by
          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8
    Expected type: Thrist k a x
      Actual type: Thrist k a '(i0, k0)
    In the expression: ax :- Nil
    In an equation for `irt': irt ax = ax :- Nil
simonpj at cam-05-unx:~/tmp$


{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,
             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
             FlexibleInstances, UndecidableInstances #-}

module Knett where

class IMonad (m :: (k -> *) -> k -> *) | m -> k where
  ireturn :: a x -> m a x

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil  :: Thrist a '(i,i)
  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

-- instance IMonad Thrist where
--  ireturn a = a :- Nil

irt :: a x -> Thrist a x
irt ax = ax :- Nil


From: glasgow-haskell-users-bounces at haskell.org<mailto:glasgow-haskell-users-bounces at haskell.org> [mailto:glasgow-haskell-users-bounces at haskell.org<mailto:glasgow-haskell-users-bounces at haskell.org>] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users at haskell.org<mailto:glasgow-haskell-users at haskell.org>
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where
  ireturn :: a x -> m a x

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where
  ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where
  ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m.

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where
  ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs
ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x
ghci> :info IMonad
class IMonad k m | m -> k where
  ireturn :: a x -> m a x

But when I add

ghci> :{
Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Prelude|   Nil :: Thrist a '(i,i)
Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
    lookupVarEnv_NF: Nothing

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue.

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120831/693188b0/attachment-0001.htm>