Illegal polymorphic or qualified type using RankNTypes and TypeFamilies

Question

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…

Accepted Answer

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.

Illegal polymorphic or qualified type using RankNTypes and TypeFamilies

Solution

Problem