Does this, and should this type check on GHC 6.10.x ?

headers Ahn, Ki Yung | 26 Jun 06:47

Dear GHC type hackers,

We got a code (please refer to the attached lhs file) that uses type
families and type classes very cleverly.  We don't know who wrote
itbecause this was a contribution of an anonymous reviewer on our paper,
which we are still revising. http://kyagrd.dyndns.org/wiki/SharedSubtypes
Although we learned a lot from this code, we still have unsolved
question about this code.

The problem is, we are still not sure whether this code actually type
checks in any GHC version, and we are not even sure whether this should
type check or not as it is.  I wasn't able to type check this in any of
the GHC versions 6.10.1 on windows and debian linux, GHC 6.10.2 on
windows and debian linux, or GHC 6.10.3 on debian linux.  I also asked
some of my colleagues at my school who has GHC installed to run this
code, but they weren't able to load up either.

However, some people we email conversation with reported that they were
able to successfully load this code in GHC version 6.10.1 in their
system.  This is very surprising because we weren't able to type check
it with the same version (GHC 6.10.1) on our machines (Windows XP and
Debian Linux).  Since there is no reason that GHC type checker would
behave differently among different platforms, the code I am attaching is
still an unsolved misery to us.

It would be very helpful for us if any of can type check this successful
could report what version of GHC on what platform and what GHC command
line options used to make this code type check.  And also, we welcome
any discussion whether this code should or should not in principle type
check.

Thanks in advance,

Ahn, Ki Yung

FYI, I had the following error message when I tried it on ghc 6.10.3.
(When I commented out the problematic line, the last equation of crossB,
I was able to load it up though.  So, this code definitely doesn't seem
to be just thought out of one's mind without actually running on ghc.)

========================================================================

kyagrd <at> kyavaio:~/tmp$ ghci --version
The Glorious Glasgow Haskell Compilation System, version 6.10.3
kyagrd <at> kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances
Review3.lhs
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( Review3.lhs, interpreted )

Review3.lhs:67:29:
    Could not deduce (Expandable (Tuple (Map ((,) t2) ys)))
      from the context (xs ~ t2 ::: ts2, Expandable t2)
      arising from a use of `:::' at Review3.lhs:67:29-59
    Possible fix:
      add (Expandable (Tuple (Map ((,) t2) ys))) to the context of
        the constructor `:::'
      or add an instance declaration for
         (Expandable (Tuple (Map ((,) t2) ys)))
    In the expression: Bs (mapB x ys) ::: crossB xs ys
    In the definition of `crossB':
        crossB (x ::: xs) ys = Bs (mapB x ys) ::: crossB xs ys
    In the definition of `expandPair':
        expandPair _ pair (a ::: as) (b ::: bs)
                     = crossB (a ::: as) (b ::: bs)
                     where
                         crossB :: BList xs -> BList ys -> BList (Cross
xs ys)
                         crossB Nil ys = Nil
                         crossB (x ::: xs) ys = Bs (mapB x ys) :::
crossB xs ys
                         mapB ::
                           (Expandable x) => Bit x -> BList ys -> BList
(Map ((,) x) ys)
                         mapB x Nil = Nil
                         mapB x (y ::: ys) = pair x y ::: mapB x ys
Failed, modules loaded: none.