I ran into this same issue in my own experimentation: if a type variable x has
a kind with only one constructor K, GHC does not supply the equality x ~ K y
for some fresh type variable y. Perhaps it should. I too had to use similar
workarounds to what you have come up with.
One potential problem is the existence of the Any type, which inhabits every
kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an
inconsistent coercion (equating two types with distinct ground head types).
However, because the RHS is a promoted datatype, we know that this coercion can
never be applied to a term. Because equality is homogeneous (i.e. ~ can relate
only two types of the same kind), I'm not convinced the existence of Any ~ K y
is so bad. (Even with heterogeneous equality, it might work out, given that
there is more than one type constructor that results in *...)
Regarding the m -> k fundep: my experiments suggest that this dependency is
implied when you have (m :: k), but I guess not when you have k appear in the
kind of m in a more complicated way. Currently, there are no kind-level
functions, so it appears that m -> k could be implied whenever k appears
anywhere in the kind of m. If (when!) there are kind-level functions, we'll
have to be more careful.
Richard
On Aug 31, 2012, at 9:06 AM, Edward Kmett wrote:
> This works, though it'll be all sorts of fun to try to scale up.
>
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
> DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
> TypeFamilies #-}
> module Indexed.Test where
>
> class IMonad (m :: (k -> *) -> k -> *) | m -> k
> where ireturn :: a x -> m a x
>
> type family Fst (a :: (p,q)) :: p
> type instance Fst '(p,q) = p
>
> type family Snd (a :: (p,q)) :: q
> type instance Snd '(p,q) = q
>
> infixr 5 :-
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
> Nil :: Thrist a '(i,i)
> (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij ->
> Thrist a jk -> Thrist a ik
>
> instance IMonad Thrist where
> ireturn a = a :- Nil
>
> I know Agda has to jump through some hoops to make the refinement work on
> pairs when they do eta expansion. I wonder if this could be made less painful.
>
>
> On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett <ekm...@gmail.com> wrote:
> Hrmm. This seems to work manually for getting product categories to work.
> Perhaps I can do the same thing for thrists.
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
> module Product where
>
> import Prelude hiding (id,(.))
>
> class Category k where
> id :: k a a
> (.) :: k b c -> k a b -> k a c
>
> type family Fst (a :: (p,q)) :: p
> type instance Fst '(p,q) = p
>
> type family Snd (a :: (p,q)) :: q
> type instance Snd '(p,q) = q
>
> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
> (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b
>
> instance (Category x, Category y) => Category (x * y) where
> id = id :* id
> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>
>
>
> On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett <ekm...@gmail.com> wrote:
> 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 <simo...@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@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-boun...@haskell.org
> [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of Edward Kmett
> Sent: 31 August 2012 03:38
> To: glasgow-haskell-users@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
>
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
