PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Dan Doel]

On Fri, Aug 31, 2012 at 9:06 AM, Edward Kmett <ekmett at gmail.com> wrote:
> 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.

To flesh this out slightly, there are two options for defining pairs in Agda:

  data Pair1 (A B : Set) : Set where
    _,_ : A -> B -> Pair1 A B

  record Pair2 (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

Now, if we have something similar to Thrist indexed by Pair2, we have
no problems, because:

    A p -> M A p

is equal to:

    A (fst p , snd p) -> M A (fst p , snd p)

Which is what we need for the irt definition to make sense. If we
index by Pair1, this won't happen automatically, but we have an
alternate definition of irt:

    irt : {I J : Set} {A : Pair1 I J -> Set} {p : Pair1 I J} -> A p ->
Thrist A p
    irt {I} {J} {A} {i , j} ap = ap :- Nil

The pattern match {i , j} there refines p to be (i , j) everywhere, so
the definition is justified.

Without one of these two options, these definitions seem like they're
going to be cumbersome. Ed seems to have found a way to do it, by what
looks kind of like hand implementing the record version, but it looks
unpleasant.

On another note, it confuses me that m -> k would be necessary at all
in the IMonad definition. k is automatically determined by being part
of the kind of m, and filling in anything else for k would be a type
error, no? It is the same kind of reasoning that goes on in
determining what 'a' is for 'id :: forall a. a -> a' based on the type
of the first argument.

-- Dan