Illegal polymorphic or qualified type using RankNTypes and TypeFamilies

11
votes

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)
2
haskelltype-families
Comment for random passers by: the above Illegal polymorphic type error is documented in haskell.org/ghc/docs/latest/html/users_guide/… – Chris Kuklewicz
I'm not sure of this, but is the precedence of forall such that (forall (c :: Const) . Value c a) -> CallArgs b is different to forall (c :: Const) . Value c a -> CallArgs? (i.e. grouping the forall more tightly.) – huon
@dbaupp: forall is a variable binding construct, like a lambda, and has essentially the same "precedence"--its scope extends as far to the right as syntactically possible. – C. A. McCann
@dbaupp I updated the question. I don't think it fundamentally alters the question though as neither case is supported. – Nathan Howell
@NathanHowell Oh, that edit is very surprising! Do you want CallArgs (a -> b) to represent a function that can accept either a Value 'Const a or a Value 'Variable a as its first argument (at the discretion of the person calling the function) or to represent a function that accepts as its first argument a value that can be either a Value 'Const a or a Value 'Variable a (at the discretion of the function itself)? If the latter, my answer probably needs a bit of an update. – Daniel Wagner

2 Answers

6
votes

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.

3
votes

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)