Mon Dec 5 22:08:24 EST 2011


I've seen this before.  Using :t at the GHCi prompt gives a different
type signature than specified:

*Main> :t _lambda
  :: (Loop s m r, StructPair (,) r, StructPrim s r as) =>
     (r as -> m (r t)) -> m (r (as -> m t))

class TML m r => Loop s m r | r -> m, r -> s where
  _lambda :: (Struct s r as ras) 
             => (ras -> m (r t))
             -> m (r (as -> m t))

After a night of sleep..  I removed the -XIncoherentInstances and I
get an error:

    Overlapping instances for Struct s r a (r a)
      arising from a use of `_lambda'
    Matching instances:
      instance [overlap ok] (StructPrim s r t, StructPair (,) r) =>
                            Struct s r t (r t)
        -- Defined at Loop.hs:(130,10)-(132,30)
      instance [overlap ok] (StructPair (,) r,
                             Struct s r as r_as,
                             Struct s r bs r_bs) =>
                            Struct s r (as, bs) (r_as, r_bs)
        -- Defined at Loop.hs:(111,10)-(114,43)
    (The choice depends on the instantiation of `r, s, a'
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: _lambda
    In the expression: _lambda $ \ (a, b) -> _ret a
    In an equation for `f7': f7 = _lambda $ \ (a, b) -> _ret a

This is strange because the Prim/Pair heads should really be

Following [1] it says that GHC does not take into account the context
of a rule when matching.  Then -XOverlappingInstances makes it
possible to have multiple matches as long as there is a specific one,
and -XIncoherentInstances a choice is forced to pick the more general
instance at compile time of a generic function when possibly that
function might be specialized later and a more specific one would
match.  It looks like that is where the trouble comes from.  Somehow
one of these is chosen at a time when it shouldn't be:

instance (StructPair (,) r, 
          Struct s r as r_as,
          Struct s r bs r_bs)
         => Struct s r (as,bs) (r_as, r_bs) where

instance (StructPrim s r t,
          StructPair (,) r)
         => Struct s r t (r t) where  

The second one is clearly more general, and this is indeed what the
error message suggests.

So.. How to fix that?  Maybe it's a good idea to construct some
simpler example that has the same problem and ask it on the Haskell

If I recall I saw some trick that used an extra type argument to
disambiguate the heads.  Maybe this can be used here too?

I run into fundep problems, so let's try to simplify it a bit.

I removed the (,) argument in StructPair.  By adding an explicit tag
that reflects the basic structure of the instance, i.e. () ((),()),
... I was able to at least make an unambiguous instance, but the
trouble then is to invoke it, because the type needs to be known!
Maybe this is the whole overlapping/existential thing?

Ok, I'm getting into random mutation territory.  I removed the tagging
and now I get to a point where I can't instantiate multiple
representations in the same module, probably by changing one of the

  as -> r ras, ras -> r as, r -> stx

which is of course incorrect..  It should be:

  r as -> ras, ras -> r as, r -> stx

this brings me back to square one.

Maybe it's just necessary to properly tag the "atom" in the struct
such that a tree node and a leaf node cannot be confused.  ( Then
after that works it might be possible to write something on top of
that to make argument lists easier to use. )

Similar problems..  It disambiguates some things, but now I can't make
a fundep ras -> r as because this will fix r.  Maybe only fundep ras
-> as and fix r in another way?

Ok, there was a bug!  It should be 

   Struct s r (StructAtom t) (StructAtom (r t)) where

instead of

   Struct s r (StructAtom t) (r (StructAtom t)) where

and StructPair should have the `atom' and `unatom' bijection that
commutes the StructAtom tag with the representation.

Following that through it seems to be clear what's going on now, at
the expense of some verbosity in the HOAS as it's littered with Cons
and Atom constructors.

Most type annotations in Loop_test_arity.hs can now also be removed.

[1] http://www.haskell.org/ghc/docs/6.6/html/users_guide/type-extensions.html