#2627: GADT + Type family doesn't unify like I expect
-------------------------------------+--------------------------------------
Reporter: ryani | Owner: chak
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.9
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-------------------------------------+--------------------------------------
Changes (by simonpj):
* owner: => chak
* difficulty: => Unknown
Comment:
Nice example -- just the kind of interaction between GADTs and type
functions that should now work. I've convinced myself that your code
should indeed compile.
I stripped out a couple of eqns in the example, and wrote out the
derivation that shows it should typecheck.
Manuel, over to you!
Simon
{{{
conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
conn (Rd k) (Wr a r) = conn (k a) r
-- conn (Fin x) (Fin y) = (x,y)
-- conn (Wr a r) (Rd k) = conn r (k a)
{- Simon's reasoning
Given :: Dual a ~ b, Dual b ~ a (sig)
a ~ R a1 b1, b ~ W a2 b2 (gadt match)
k :: a1 -> Con b1
a :: a2
r :: Conn b2
Instantiate conn at: ai, bi (unification variables)
Wanted: Dual ai ~ bi, Dual bi ~ ai
first arg: a1~a2, b1~ai
second: b2~bi
Fixing the unification variables is easy: ai:=b1, bi:=b2
The interesting thing is figuring out that a1~a2
Wanted: a1~a2
Given: Dual a ~ b
=> (substitute for a) Dual (R a1 b1) ~ b
=> (top-level eqn) W a1 (Dual b1) ~ b
=> (substitute for b) W a1 (Dual b1) ~ W a2 b2
=> (decompose) a1~a2
-}
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2627#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
