Illegal polymorphic or qualified type using RankNTypes and TypeFamilies
I've been slowly working on porting the llvm package to use data kinds, type families and type-nats and ran into a minor issue when trying to remove the two newtypes used for classifying values ( ConstValue and Value ) by introducing a new Value type parameterized by its constness.
CallArgs only accepts Value 'Variable a arguments and provides a function for casting a Value 'Const a to a Value 'Variable a . I'd like to generalize CallArgs to allow each argument to be either 'Const or 'Variable . Is this possible to encode this somehow using type families? I think it's probably doable with fundeps.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
data Const = Const | Variable
data Value (c :: Const) (a :: *)
type family CallArgs a :: *
type instance CallArgs (a -> b) = forall (c :: Const) . Value c a -> CallArgs b
type instance CallArgs (IO a) = IO (Value 'Variable a)
... which fails to compile:
/tmp/blah.hs:10:1:
Illegal polymorphic or qualified type:
forall (c :: Const). Value c a
In the type instance declaration for `CallArgs'
Where the following solution works (equivalent to the legacy code), but requires the user to cast the each constant Value :
type family CallArgs' a :: *
type instance CallArgs' (a -> b) = Value 'Variable a -> CallArgs' b
type instance CallArgs' (IO a) = IO (Value 'Variable a)
The CallArgs you're asking for is kind of like a non-deterministic function which takes a -> b and returns either Value 'Const a -> blah or Value 'Variable a -> blah . One thing you can sometimes to with nondeterministic functions is flip them around; indeed, this one has a deterministic inverse.
type family UnCallArgs a
type instance UnCallArgs (Value c a -> b) = a -> UnCallArgs b
type instance UnCallArgs (IO 'Variable a) = IO a
Now, anywhere you would have written a type like
foo :: CallArgs t -> LLVM t
or something like that, you can write this instead:
foo :: t -> LLVM (UnCallArgs t)
Of course, you might want to pick a better name than UnCallArgs , maybe Native or something like that, but doing that well requires a bit of domain knowledge that I don't have.
Would wrapping the forall c. in a newtype AV work for you?
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
data CV = Const | Variable
data Value (c :: CV) (a :: *)
data AV a = AV (forall c. Value c a)
type family CallArgs a :: *
type instance CallArgs (a -> b) = AV a -> CallArgs b
type instance CallArgs (IO a) = IO (Value 'Variable a)
上一篇: 如何使用GHC.TypeLits中的比较