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
