GHC: Ticket #1722: Code using type synonym families requires workarounds to compile
http://ghc.haskell.org/trac/ghc/ticket/1722
<p>
I am trying to use type synonym families to create GADTs that can be used interchangably as both typed and untyped ASTs for a small programming language. Here are the (cut down & simplified) definitions:
</p>
<pre class="wiki">data Typed
data Untyped
type family TU a b :: *
type instance TU Typed b = b
type instance TU Untyped b = ()
-- A type witness type, use eg. for pattern-matching on types
data Type a where
TypeInt :: Type Int
TypeBool :: Type Bool
TypeString :: Type String
TypeList :: Type t -> Type [t]
data Expr :: * -> * -> * {- tu a -} where
Const :: Type a -> a -> Expr tu (TU tu a)
Var2 :: String -> TU tu (Type a) -> Expr tu (TU tu a)
</pre><p>
It mostly works, which still amazes me, but there are some small glitches. For example in some cases I have to use <strong>(TU Typed Bool)</strong> instead of
<strong>Bool</strong>, even if they should be equal (<strong>type instance TU Typed b = b</strong>). In other cases I have to artificially restrict or generalize functions' type signatures. Or I have to put type signatures in patterns. The biggest problem is that it isn't obvious which workaround is needed in a given case. For some cases I don't have a satisfactory workaround yet.
</p>
<p>
Perhaps these problems simply reflect immaturity of type synonym family support in GHC, but, on the other hand, it may be some simple bug which could be fixed for GHC 6.8.
</p>
<p>
I've created a set of test files which I will attach to this ticket. Run check.sh to see how GHC handles the original (inteded) code and the workarounds. But first set the path to ghc in the script.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/1722
Trac 1.0.1guestThu, 20 Sep 2007 12:42:59 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/1722
http://ghc.haskell.org/trac/ghc/ticket/1722
<ul>
<li><strong>attachment</strong>
set to <em>bug.tar.gz</em>
</li>
</ul>
TicketguestThu, 20 Sep 2007 12:43:56 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:1
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:1
<ul>
<li><strong>cc</strong>
<em>tomasz.zielonka@…</em> added
</li>
</ul>
TicketchakWed, 26 Sep 2007 09:18:55 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:2
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:2
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
</ul>
TicketchakSat, 29 Sep 2007 12:15:42 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:3
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:3
<ul>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
<p>
Currently, the example programs fail in code that is related to the GADT refinement story, which we are planning to remove anyway soon. I will re-evaluate the situation once GADT refinement in GHC is implemented by equality constraints.
</p>
TicketchakTue, 11 Dec 2007 06:31:30 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:4
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:4
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>indexed-types/should_compile/GADT12</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
As expected, the replacement of GADT refinement with equality constraints fixed this bug. More precisely, the test cases <tt>Bug1</tt>, <tt>Bug2A</tt>, and <tt>Bug2B</tt> are working now. The module Bug3 is still rejected:
</p>
<pre class="wiki">Code:
module Bug3 where
import Defs
bug :: Expr Typed a -> ()
bug (Var2 "x" (TypeList TypeBool :: Type [Bool])) = ()
bug e = ()
Compilation:
[1 of 2] Compiling Defs ( Defs.hs, Defs.o )
[2 of 2] Compiling Bug3 ( Bug3.hs, Bug3.o )
Bug3.hs:13:15:
Couldn't match expected type `a2' against inferred type `[Bool]'
`a2' is a rigid type variable bound by
the constructor `Var2' at Bug3.hs:13:5
Expected type: TU Typed (Type a2)
Inferred type: Type [Bool]
In the pattern: TypeList TypeBool :: Type [Bool]
In the pattern: Var2 "x" (TypeList TypeBool :: Type [Bool])
</pre><p>
However, I believe this program is actually incorrect; i.e., GHC rightfully rejects it.
</p>
<p>
Interestingly, the test cases that I added to the regression test suite does trigger a corelint failure. This is however a different bug; hence, I am closing this one.
</p>
TicketsimonmarTue, 30 Sep 2008 15:40:21 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:5
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:5
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:29 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:6
http://ghc.haskell.org/trac/ghc/ticket/1722#comment:6
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
Ticket