Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. +--- Reporter: jeltsch| Owner: Type: bug| Status: closed Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Resolution: fixed | Keywords: Testcase: T1999, T1999a | Blockedby: Difficulty: Unknown| Os: Linux Blocking: | Architecture: x86 Failure: None/Unknown | +--- Changes (by simonpj): * status: new = closed * resolution: = fixed Comment: Stop press. Jim's program (test `gadt/termination`) is actually just fine. It was not failing because of the FC changes above, but rather because of an outright bug, now checked by `typecheck/should_compile/GivenTypeSynonym`. So I'll close this ticket. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc.
+---
Reporter: jeltsch| Owner: chak
Type: bug| Status: closed
Priority: normal | Milestone: 6.10 branch
Component: Compiler |Version: 6.9
Resolution: fixed | Keywords:
Testcase: T1999, T1999a | Blockedby:
Difficulty: Unknown| Os: Linux
Blocking: | Architecture: x86
Failure: None/Unknown |
+---
Changes (by simonpj):
* failure: = None/Unknown
Comment:
Here is another example of the usefulness of decomposing type
applications, due to Jim Apple, and recorded in test `gadt/termination`:
{{{
{-# 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 ::
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc.
+---
Reporter: jeltsch| Owner:
Type: bug| Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler |Version: 6.9
Resolution: | Keywords:
Testcase: T1999, T1999a | Blockedby:
Difficulty: Unknown| Os: Linux
Blocking: | Architecture: x86
Failure: None/Unknown |
+---
Changes (by simonpj):
* cc: sweirich@…, jbapple@…, byorgey@… (added)
* owner: chak =
* status: closed = new
* resolution: fixed =
Old description:
The following code causes a panic with GHC installed from
ghc-6.9.20071218-i386-unknown-linux.tar.bz2:
{{{
{-# 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)
}}}
The output of ghci is:
{{{
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]
predb{tv anB} [sk] ~ b{tv aoc} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
The output of ghc -c is:
{{{
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]
predb{tv a5O} [sk] ~ b{tv a6p} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
New description:
The following code causes a panic with GHC installed from
ghc-6.9.20071218-i386-unknown-linux.tar.bz2:
{{{
{-# 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)
}}}
The output of ghci is:
{{{
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]
predb{tv anB} [sk] ~ b{tv aoc} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
The output of ghc -c is:
{{{
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]
predb{tv a5O} [sk] ~ b{tv a6p} [sk]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}}
--
Comment:
In our POPL paper [http://research.microsoft.com/en-
us/um/people/simonpj/papers/ext-f/popl163af-weirich.pdf Generative type
abstraction and type-level computation] we proposed to '''remove the
ability to decomopose type applications'''. So Ganesh's example above
would not work any more:
{{{
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
}}}
Neither would Jim Apple's example.
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 ''inference'' 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.
Dimitrios and I think that it'd be possible to re-add `left` and `right`
coercions, without too much hassle (and re-add the saturated-type-function
reqt to FC). Stephanie, Brent: do you agree?
Meanwhile, Gasnesh, Jim, how much do you care?
All this relates to the `ghc-new-co` branch, which will shortly become the
master, so it's of more than theoretical interest.
Simon
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. +--- Reporter: jeltsch| Owner: Type: bug| Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Resolution: | Keywords: Testcase: T1999, T1999a | Blockedby: Difficulty: Unknown| Os: Linux Blocking: | Architecture: x86 Failure: None/Unknown | +--- Changes (by simonpj): * cc: dimitris@… (added) -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc.
+---
Reporter: jeltsch| Owner:
Type: bug| Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler |Version: 6.9
Resolution: | Keywords:
Testcase: T1999, T1999a | Blockedby:
Difficulty: Unknown| Os: Linux
Blocking: | Architecture: x86
Failure: None/Unknown |
+---
Comment(by japple):
I don't really understand the implications of this yet. In Cheney
Hinze's [http://ecommons.cornell.edu/handle/1813/5614 First-Class Phantom
Types] there is an example that this change might break:
{{{
{-# 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)
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:14
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. +--- Reporter: jeltsch| Owner: Type: bug| Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Resolution: | Keywords: Testcase: T1999, T1999a | Blockedby: Difficulty: Unknown| Os: Linux Blocking: | Architecture: x86 Failure: None/Unknown | +--- Comment(by ganesh): Jim: I think that case is ok because there's no free variable being used as a type constructor. 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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. +--- Reporter: jeltsch| Owner: Type: bug| Status: new Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Resolution: | Keywords: Testcase: T1999, T1999a | Blockedby: Difficulty: Unknown| Os: Linux Blocking: | Architecture: x86 Failure: None/Unknown | +--- Comment(by japple): 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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler ___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. ---+ Reporter: jeltsch| Owner: chak Type: bug| Status: closed Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal | Resolution: fixed Keywords: | Difficulty: Unknown Testcase: T1999, T1999a | Architecture: x86 Os: Linux | ---+ Changes (by chak): * status: reopened = closed * resolution: = fixed Comment: Fixed with the new equality solver. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. ---+ Reporter: jeltsch| Owner: chak Type: bug| Status: reopened Priority: normal | Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal | Resolution: Keywords: | Difficulty: Unknown Testcase: T1999, T1999a | Architecture: x86 Os: Linux | ---+ Changes (by simonpj): * testcase: T1999 = T1999, T1999a -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc.
--+-
Reporter: jeltsch | Owner: chak
Type: bug | Status: reopened
Priority: normal| Milestone: 6.10 branch
Component: Compiler |Version: 6.9
Severity: normal| Resolution:
Keywords:| Difficulty: Unknown
Testcase: T1999 | Architecture: x86
Os: Linux |
--+-
Comment (by ganesh):
{{{
{-# 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
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: reopened Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase: T1999 | Architecture: x86 Os: Linux | --+- Changes (by ganesh): * cc: [EMAIL PROTECTED] (added) Comment: 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. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: reopened Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase: T1999 | Architecture: x86 Os: Linux | --+- Comment (by chak): Replying to [comment:6 ganesh]: 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. That might be useful, so that if it has a different cause, we can make sure to fix your problem, too. Thanks. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: reopened Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase: T1999 | Architecture: x86 Os: Linux | --+- Changes (by chak): * testcase: = T1999 * status: closed = reopened * resolution: fixed = Comment: I spoke too early. Reopened. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: reopened Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase: T1999 | Architecture: x86 Os: Linux | --+- Comment (by chak): More precisely, the error only occurs with -dcore-lint (which is why I at first thought it was fixed). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: closed Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: fixed Keywords:| Difficulty: Unknown Testcase:| Architecture: x86 Os: Linux | --+- Changes (by chak): * status: new = closed * resolution: = fixed Comment: Works with the new GADT machinery based on equalities. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: chak Type: bug | Status: new Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase:| Architecture: x86 Os: Linux | --+- Changes (by simonpj): * owner: = chak Comment: 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. So I'm assigning this to Manuel; it'd be good to make a test case out of it too. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #1999: panic with GADT etc.
#1999: panic with GADT etc. --+- Reporter: jeltsch | Owner: Type: bug | Status: new Priority: normal| Milestone: 6.10 branch Component: Compiler |Version: 6.9 Severity: normal| Resolution: Keywords:| Difficulty: Unknown Testcase:| Architecture: x86 Os: Linux | --+- Changes (by igloo): * milestone: = 6.10 branch Comment: Thanks for the report! This works in 6.8.2. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/1999#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
