GHC: Ticket #1999: panic with GADT etc.
http://ghc.haskell.org/trac/ghc/ticket/1999
<p>
The following code causes a panic with GHC installed from ghc-6.9.20071218-i386-unknown-linux.tar.bz2:
</p>
<pre class="wiki">{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs #-}
module Bug where
class C a where
f :: G a -> ()
instance (C ()) => C (b c) where
f (G x) = f x where
data G a where
G :: G () -> G (b c)
</pre><p>
The output of ghci is:
</p>
<pre class="wiki">GHCi, version 6.9.20071218: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc-6.9.20071218: panic! (the 'impossible' happened)
(GHC version 6.9.20071218 for i386-unknown-linux):
Coercion.splitCoercionKindOf
base:GHC.Prim.left{(w) tc 34B} $co${tc aog} [tv]
<pred>b{tv anB} [sk] ~ b{tv aoc} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
</pre><p>
The output of ghc -c is:
</p>
<pre class="wiki">ghc-6.9.20071218: panic! (the 'impossible' happened)
(GHC version 6.9.20071218 for i386-unknown-linux):
Coercion.splitCoercionKindOf
base:GHC.Prim.left{(w) tc 34B} $co${tc a6t} [tv]
<pred>b{tv a5O} [sk] ~ b{tv a6p} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/1999
Trac 1.0.1iglooTue, 01 Jan 2008 16:41:55 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:1
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:1
<ul>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
<p>
Thanks for the report! This works in 6.8.2.
</p>
TicketsimonpjThu, 03 Jan 2008 14:40:37 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:2
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:2
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
</ul>
<p>
However, it may well not work in the HEAD, where Manuel is busy ripping out the old implementation of GADTs, in favour of the new type-function-based machinery.
</p>
<p>
So I'm assigning this to Manuel; it'd be good to make a test case out of it too.
</p>
<p>
Simon
</p>
TicketchakSat, 05 Jul 2008 03:59:09 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:3
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:3
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Works with the new GADT machinery based on equalities.
</p>
TicketchakWed, 09 Jul 2008 07:00:04 GMTstatus changed; testcase set; resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:4
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:4
<ul>
<li><strong>status</strong>
changed from <em>closed</em> to <em>reopened</em>
</li>
<li><strong>testcase</strong>
set to <em>T1999</em>
</li>
<li><strong>resolution</strong>
<em>fixed</em> deleted
</li>
</ul>
<p>
I spoke too early. Reopened.
</p>
TicketchakWed, 09 Jul 2008 07:04:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:5
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:5
<p>
More precisely, the error only occurs with -dcore-lint (which is why I at first thought it was fixed).
</p>
TicketganeshSun, 17 Aug 2008 13:30:45 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:6
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:6
<ul>
<li><strong>cc</strong>
<em>ganesh@…</em> added
</li>
</ul>
<p>
I'm also getting this error (without -dcore-lint, or at least without explicitly specifying it); if it's useful I can cut down a test case.
</p>
TicketchakMon, 18 Aug 2008 02:34:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:7
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:7
<p>
Replying to <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/1999#comment:6" title="Comment 6 for Ticket #1999">ganesh</a>:
</p>
<blockquote class="citation">
<p>
I'm also getting this error (without -dcore-lint, or at least without explicitly specifying it); if it's useful I can cut down a test case.
</p>
</blockquote>
<p>
That might be useful, so that if it has a different cause, we can make sure to fix your problem, too. Thanks.
</p>
TicketganeshMon, 18 Aug 2008 19:49:02 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:8
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:8
<pre class="wiki">{-# LANGUAGE GADTs #-}
module Types where
data EqTypes a b where
EqConstr :: EqTypes a b -> EqTypes (s a) (s b)
eqUnConstr :: EqTypes (s a) (s b) -> EqTypes a b
eqUnConstr (EqConstr eq) = eq
</pre>
TicketsimonpjTue, 02 Sep 2008 12:15:00 GMTtestcase changed
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:9
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:9
<ul>
<li><strong>testcase</strong>
changed from <em>T1999</em> to <em>T1999, T1999a</em>
</li>
</ul>
TicketchakTue, 16 Sep 2008 12:55:26 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:10
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:10
<ul>
<li><strong>status</strong>
changed from <em>reopened</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Fixed with the new equality solver.
</p>
TicketsimonpjMon, 09 May 2011 10:19:29 GMTfailure set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:11
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:11
<ul>
<li><strong>failure</strong>
set to <em>None/Unknown</em>
</li>
</ul>
<p>
Here is another example of the usefulness of decomposing type applications, due to Jim Apple, and recorded in test <tt>gadt/termination</tt>:
</p>
<pre class="wiki">{-# LANGUAGE GADTs, Rank2Types #-}
module Termination where
{- Message from Jim Apple to Haskell-Cafe, 7/1/07
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
Using GADTs to encode normalizable and non-normalizable terms in
the lambda calculus. For definitions of normalizable and de Bruin
indices, I used:
Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of
de Bruijn Indices and Names. In Proceedings of the International
Workshop on Logical Frameworks and Meta-Languages: Theory and
Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59
http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps
@incollection{ pierce97foundational,
author = "Benjamin Pierce",
title = "Foundational Calculi for Programming Languages",
booktitle = "The Computer Science and Engineering Handbook",
publisher = "CRC Press",
address = "Boca Raton, FL",
editor = "Allen B. Tucker",
year = "1997",
url = "citeseer.ist.psu.edu/pierce95foundational.html"
}
> So it sounds to me like the (terminating) type checker solves the
> halting problem. Can you please explain which part of this I have
> misunderstood?
The Terminating datatype takes three parameters:
1. A term in the untyped lambda calculus
2. A sequence of beta reductions
3. A proof that the result of the beta reductions is normalized.
Number 2 is the hard part. For a term that calculated the factorial of
5, the list in part 2 would be at least 120 items long, and each one
is kind of a pain.
GHC's type checker ends up doing exactly what it was doing before:
checking proofs.
-}
-- Terms in the untyped lambda-calculus with the de Bruijn representation
data Term t where
Var :: Nat n -> Term (Var n)
Lambda :: Term t -> Term (Lambda t)
Apply :: Term t1 -> Term t2 -> Term (Apply t1 t2)
-- Natural numbers
data Nat n where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
data Z
data S n
data Var t
data Lambda t
data Apply t1 t2
data Less n m where
LessZero :: Less Z (S n)
LessSucc :: Less n m -> Less (S n) (S m)
data Equal a b where
Equal :: Equal a a
data Plus a b c where
PlusZero :: Plus Z b b
PlusSucc :: Plus a b c -> Plus (S a) b (S c)
{- We can reduce a term by function application, reduction under the lambda,
or reduction of either side of an application. We don't need this full
power, since we could get by with normal-order evaluation, but that
required a more complicated datatype for Reduce.
-}
data Reduce t1 t2 where
ReduceSimple :: Replace Z t1 t2 t3 -> Reduce (Apply (Lambda t1) t2) t3
ReduceLambda :: Reduce t1 t2 -> Reduce (Lambda t1) (Lambda t2)
ReduceApplyLeft :: Reduce t1 t2 -> Reduce (Apply t1 t3) (Apply t2 t3)
ReduceApplyRight :: Reduce t1 t2 -> Reduce (Apply t3 t1) (Apply t3 t2)
{- Lift and Replace use the de Bruijn operations as expressed in the Urban
and Berghofer paper. -}
data Lift n k t1 t2 where
LiftVarLess :: Less i k -> Lift n k (Var i) (Var i)
LiftVarGTE :: Either (Equal i k) (Less k i) -> Plus i n r -> Lift n k (Var i) (Var r)
LiftApply :: Lift n k t1 t1' -> Lift n k t2 t2' -> Lift n k (Apply t1 t2) (Apply t1' t2')
LiftLambda :: Lift n (S k) t1 t2 -> Lift n k (Lambda t1) (Lambda t2)
data Replace k t n r where
ReplaceVarLess :: Less i k -> Replace k (Var i) n (Var i)
ReplaceVarEq :: Equal i k -> Lift k Z n r -> Replace k (Var i) n r
ReplaceVarMore :: Less k (S i) -> Replace k (Var (S i)) n (Var i)
ReplaceApply :: Replace k t1 n r1 -> Replace k t2 n r2 -> Replace k (Apply t1 t2) n (Apply r1 r2)
ReplaceLambda :: Replace (S k) t n r -> Replace k (Lambda t) n (Lambda r)
{- Reflexive transitive closure of the reduction relation. -}
data ReduceEventually t1 t2 where
ReduceZero :: ReduceEventually t1 t1
ReduceSucc :: Reduce t1 t2 -> ReduceEventually t2 t3 -> ReduceEventually t1 t3
-- Definition of normal form: nothing with a lambda term applied to anything.
data Normal t where
NormalVar :: Normal (Var n)
NormalLambda :: Normal t -> Normal (Lambda t)
NormalApplyVar :: Normal t -> Normal (Apply (Var i) t)
NormalApplyApply :: Normal (Apply t1 t2) -> Normal t3 -> Normal (Apply (Apply t1 t2) t3)
-- Something is terminating when it reduces to something normal
data Terminating where
Terminating :: Term t -> ReduceEventually t t' -> Normal t' -> Terminating
{- We can encode terms that are non-terminating, even though this set is
only co-recursively enumerable, so we can't actually prove all of the
non-normalizable terms of the lambda calculus are non-normalizable.
-}
data Reducible t1 where
Reducible :: Reduce t1 t2 -> Reducible t1
-- A term is non-normalizable if, no matter how many reductions you have applied,
-- you can still apply one more.
type Infinite t1 = forall t2 . ReduceEventually t1 t2 -> Reducible t2
data NonTerminating where
NonTerminating :: Term t -> Infinite t -> NonTerminating
-- x
test1 :: Terminating
test1 = Terminating (Var Zero) ReduceZero NormalVar
-- (\x . x)@y
test2 :: Terminating
test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero))
(ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE (Left Equal) PlusZero))) ReduceZero)
NormalVar
-- omega = \x.x@x
type Omega = Lambda (Apply (Var Z) (Var Z))
omega = Lambda (Apply (Var Zero) (Var Zero))
-- (\x . \y . y)@(\z.z@z)
test3 :: Terminating
test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)
(ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess LessZero))) ReduceZero)
(NormalLambda NormalVar)
-- (\x.x@x)(\x.x@x)
test4 :: NonTerminating
test4 = NonTerminating (Apply omega omega) help3
help1 :: Reducible (Apply Omega Omega)
help1 = Reducible (ReduceSimple
(ReplaceApply (ReplaceVarEq Equal (LiftLambda
(LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero))))
(ReplaceVarEq Equal (LiftLambda (LiftApply
(LiftVarLess LessZero) (LiftVarLess LessZero))))))
help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t
help2 ReduceZero = Equal
help2 (ReduceSucc (ReduceSimple (ReplaceApply
(ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _))))
(ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y)
= case help2 y of
Equal -> Equal
help3 :: Infinite (Apply Omega Omega)
help3 x = case help2 x of
Equal -> help1
</pre>
TicketsimonpjMon, 09 May 2011 10:33:08 GMTcc, status, description changed; owner, resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:12
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:12
<ul>
<li><strong>cc</strong>
<em>sweirich@…</em> <em>jbapple@…</em> <em>byorgey@…</em> added
</li>
<li><strong>owner</strong>
<em>chak</em> deleted
</li>
<li><strong>status</strong>
changed from <em>closed</em> to <em>new</em>
</li>
<li><strong>resolution</strong>
<em>fixed</em> deleted
</li>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/1999?action=diff&version=12">diff</a>)
</li>
</ul>
<p>
In our POPL paper <a class="ext-link" href="http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/popl163af-weirich.pdf"><span class="icon"></span>Generative type abstraction and type-level computation</a> we proposed to <strong>remove the ability to decomopose type applications</strong>. So Ganesh's example above would not work any more:
</p>
<pre class="wiki">data EqTypes a b where
EqConstr :: EqTypes a b -> EqTypes (s a) (s b)
eqUnConstr :: EqTypes (s a) (s b) -> EqTypes a b
eqUnConstr (EqConstr eq) = eq
</pre><p>
Neither would Jim Apple's example.
</p>
<p>
This is an un-forced change, and it does reduce expressiveness slightly, with no workaround. On the other hand, it does undoubtedly make things a bit simpler and, as Section 6.2 of the paper says, it allows FC to have un-saturated type functions. BUT for type <em>inference</em> we still need saturated type functions, so allowing un-saturated type functions in the intermediate language only a theoretical improvement -- programmers don't see the benefit.
</p>
<p>
Dimitrios and I think that it'd be possible to re-add <tt>left</tt> and <tt>right</tt> coercions, without too much hassle (and re-add the saturated-type-function reqt to FC). Stephanie, Brent: do you agree?
</p>
<p>
Meanwhile, Gasnesh, Jim, how much do you care?
</p>
<p>
All this relates to the <tt>ghc-new-co</tt> branch, which will shortly become the master, so it's of more than theoretical interest.
</p>
<p>
Simon
</p>
TicketsimonpjMon, 09 May 2011 10:35:21 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:13
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:13
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> added
</li>
</ul>
TicketjappleMon, 09 May 2011 15:14:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:14
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:14
<p>
I don't really understand the implications of this yet. In Cheney & Hinze's <a class="ext-link" href="http://ecommons.cornell.edu/handle/1813/5614"><span class="icon"></span>First-Class Phantom Types</a> there is an example that this change might break:
</p>
<pre class="wiki">{-# LANGUAGE GADTs #-}
module Trie where
data Trie k v where
Unit :: Maybe v -> Trie () v
Sum :: Trie k1 v -> Trie k2 v -> Trie (Either k1 k2) v
Prod :: Trie k1 (Trie k2 v) -> Trie (k1,k2) v
merge :: (v->v->v) -> Trie k v -> Trie k v -> Trie k v
merge f (Sum p q) (Sum r s) = Sum (merge f p r) (merge f q s)
</pre>
TicketganeshMon, 09 May 2011 19:59:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:15
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:15
<p>
Jim: I think that case is ok because there's no free variable being used as a type constructor.
</p>
<p>
If that understanding is correct, I can also work round this in my use case because the type constructor I want to decompose is actually statically known.
</p>
TicketjappleTue, 10 May 2011 02:19:44 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:16
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:16
<p>
Ganesh: I'm not sure "no free variable used as a type constructor" is enough to save it, since the beta-reduction code I wrote and Simon quoted doesn't use free variables as type constructors.
</p>
TicketganeshTue, 10 May 2011 06:58:00 GMT
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:17
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:17
<p>
OK, now I'm very confused about what exactly is being broken here :-)
</p>
<p>
The example given in the paper is
</p>
<pre class="wiki">data Eq a b where EQ :: Eq a a
f :: Eq (p q) (r s) → q → s
f EQ x = x
</pre><p>
As I understand it, that's dodgy if p or r are type functions, but the previous restriction on unsaturated type functions meant that couldn't arise (as I understand it). In FC2 type functions can be unsaturated but the code above is illegal because you can't decompose arbitrary type applications. But you can still decompose applications of a known datatype constructor, so I think I can still work around the restriction by just specialising my example above, replacing 's' in my example above with the actual datatype constructor needed. But as you say your beta-reduction code already seems to be using concrete datatype constructors so I must be missing something.
</p>
TicketsimonpjThu, 16 Jun 2011 14:39:45 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:18
http://ghc.haskell.org/trac/ghc/ticket/1999#comment:18
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Stop press. Jim's program (test <tt>gadt/termination</tt>) is actually just fine. It was not failing because of the FC changes above, but rather because of an outright bug, now checked by <tt>typecheck/should_compile/GivenTypeSynonym</tt>. So I'll close this ticket.
</p>
Ticket