May 2018 - ghc-tickets

[GHC] #14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'
by GHC 04 Jun '18

04 Jun '18

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)' -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This works with the [https://ghc.haskell.org/trac/ghc/ticket/2893#comment:34 latest change to the -XQuantifiedConstraints branch]. {{{#!hs {-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-} class (forall xx. (xx => a) => Implies xx b) => F a b instance (forall xx. (xx => a) => Implies xx b) => F a b class (a => b) => Implies a b instance (a => b) => Implies a b }}} but replacing `Implies xx b` with `(xx => b)` causes it to fail. I don't know if the cause of this overlaps with an existing ticket. {{{#!hs class (forall xx. (xx => a) => (xx => b)) => F a b instance (forall xx. (xx => a) => (xx => b)) => F a b -- $ ghci -ignore-dot-ghci /tmp/ASD.hs -- GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted ) -- -- /tmp/ASD.hs:4:10: error: -- • Could not deduce: xx0 -- arising from the superclasses of an instance declaration -- from the context: forall (xx :: Constraint). (xx => a, xx) => b -- bound by the instance declaration at /tmp/ASD.hs:4:10-53 -- or from: (xx => a, xx) -- bound by a quantified context at /tmp/ASD.hs:1:1 -- • In the instance declaration for ‘F a b’ -- | -- 4 | instance (forall xx. (xx => a) => (xx => b)) => F a b -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Failed, no modules loaded. -- Prelude> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14877> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 3

[GHC] #14832: QuantifiedConstraints: Strengthening context causes failure
by GHC 04 Jun '18

04 Jun '18

#14832: QuantifiedConstraints: Strengthening context causes failure -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- With Simon's latest changes (ticket:14733#comment:9) this works: {{{#!hs {-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance Refl rel => Category (With rel) where id = With (.) = undefined }}} But strengthening the context with `Trans rel`: {{{#!hs instance (Refl rel, Trans rel) => Category (With rel) where }}} causes it to fail {{{ GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( J.hs, interpreted ) J.hs:15:10: error: • Could not deduce: rel xx zz from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 or from: (rel xx yy, rel yy zz) bound by a quantified context at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ J.hs:15:10: error: • Could not deduce: rel xx xx from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14832> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 16

[GHC] #8516: Add (->) representation and the Invariant class to GHC.Generics
by GHC 04 Jun '18

04 Jun '18

#8516: Add (->) representation and the Invariant class to GHC.Generics ----------------------------------------------+---------------------------- Reporter: nfrisby | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type checker) | Version: 7.7 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Moderate (less than a day) | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: ----------------------------------------------+---------------------------- We currently disallow any use of the parameter in the domain of (->). {{{ newtype F a = F ((a -> Int) -> Int) deriving Generic1 <interactive>:4:38: Can't make a derived instance of `Generic1 (F g)': Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->) In the data declaration for `F' }}} !DeriveFunctor succeeds for this F. I'd like to add this representation type to GHC.Generics and !DeriveGeneric. {{{ newtype (f :->: g) a = FArrow1 (f a -> g a) }}} We could then represent the first example above. We could also derive the more interesting Generic1 (F g). {{{ newtype F g a = F (g a -> Int) deriving Generic1 type instance Rep1 (F g) = Rec1 g :->: Rec0 Int instance Generic1 (F g) where to x = F $ unRec0 . unArrow1 x . Rec1 from (F x) = FArrow1 $ Rec0 . x . unRec1 }}} Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon. I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim. {{{ class Invariant t where invmap :: (a -> b) -> (b -> a) -> t a -> t b invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b invmap_covariant f _ = fmap f instance (Invariant f,Invariant g) => Invariant (FArrow f g) where invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co }}} (Of course, Invariant should be a super class of Functor. :/ ) Now we can handle quite involved examples: {{{ newtype F g h a = F (g (h a)) deriving Generic1 instance Invariant g => Generic1 (F g h) where to x = invmap unRec1 Rec1 $ unComp1 x from (F x) = Comp1 $ invmap Rec1 unRec1 }}} All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8516> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 18

[GHC] #14939: StaticPointers + -dcore-lint: cause Core Lint error??
by GHC 04 Jun '18

04 Jun '18

#14939: StaticPointers + -dcore-lint: cause Core Lint error?? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple StaticPointers | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is an odd bug {{{#!hs {-# Language StaticPointers #-} import Data.Kind type Cat ob = ob -> ob -> Type type Alg cls ob = ob newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where Frí :: { with :: forall x. cls x => (a -> x) -> x } -> Frí cls a data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b) leftAdj (AlgCat f) a = undefined }}} causes a {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci -dcore-lint 222-bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 222-bug.hs, interpreted ) *** Core Lint errors : in result of Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) *** <no location info>: warning: In the type ‘forall (cls :: * -> Constraint) (b :: Alg cls *). b’ Variable escape in forall: forall (cls :: * -> Constraint) (b :: Alg cls *). b *** Offending Program *** with :: forall (cls :: * -> Constraint) a. Frí cls a -> forall x. cls x => (a -> x) -> x [LclIdX[[RecSel]], Arity=2] with .. . --->8------->8------->8--- .. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14939> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 5

[GHC] #14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’
by GHC 04 Jun '18

04 Jun '18

#14070: Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’ -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This {{{#!hs newtype M m a = M (m a) deriving newtype Functor }}} produces something similar to {{{#!hs instance Functor m => Functor (M m) where fmap :: forall a a'. (a -> a') -> (M m a -> M m a') fmap = coerce (fmap @m @a @a') }}} but as wiki:Roles2 points out, this fails for methods such as `join_`: {{{#!hs class MonadJoin m where join_ :: m (m a) -> m a newtype M m a = M (m a) deriving newtype MonadJoin -- Couldn't match representation of type ‘m (M m a)’ with that of ‘m (m a)’ }}} I think the user should be given the option to respect the roles or not by supplying `unsafe` wiki:Commentary/Compiler/DerivingStrategies {{{#!hs newtype M m a = M (m a) deriving unsafe newtype MonadJoin -- -( Produces `unsafeCoerce' instead of `coerce' )- -- instance MonadJoin m => MonadJoin (M m) where -- join_ :: forall a. M m (M m a) -> M m a -- join_ = unsafeCoerce (join_ @m @a) }}} This lets us (`newtype`-) derive a host of instances that we currently can not: `Traversable`, `Distributive` (currently forbidden due to [https://hackage.haskell.org/package/distributive-0.5.2/docs/Data- Distributive.html#v:distribute distribute]), [https://hackage.haskell.org/package/linear-1.20.7/docs/Linear- Matrix.html#v:trace Trace], [http://hackage.haskell.org/package/profunctors-5/docs/Data-Profunctor- Monad.html ProfunctorMonad / ProfunctorComonad], ... It does not seem like lenses (`FunctorWithIndex`, `FoldableWithIndex`, `TraversableWithIndex`) work with this though -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14070> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 27

[GHC] #14317: Solve Coercible constraints over type constructors
by GHC 04 Jun '18

04 Jun '18

#14317: Solve Coercible constraints over type constructors -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The core question is, could `fails` type check? {{{#!hs import Data.Type.Coercion works :: Identity a `Coercion` Compose Identity Identity a works = Coercion -- • Couldn't match representation of type ‘Identity’ -- with that of ‘Compose Identity Identity’ -- arising from a use of ‘Coercion’ -- • In the expression: -- Coercion :: Identity `Coercion` Compose Identity Identity fails :: Identity `Coercion` Compose Identity Identity fails = Coercion }}} ---- This arises from playing with [https://duplode.github.io/posts/traversable-a-remix.html Traversable: A Remix]. Given `coerce :: Compose Identity Identity ~> Identity` I wanted to capture that `id1` and `id2` are actually the same arrow (up to representation) {{{#!hs (<%<) :: (Functor f, Functor g) => (b -> g c) -> (a -> f b) -> (a -> Compose f g c) g <%< f = Compose . fmap g . f id1 :: a -> Identity a id1 = Identity id2 :: a -> Compose Identity Identity a id2 = Identity <%< Identity }}} So I define {{{#!hs data F :: (k -> Type) -> (Type -> k -> Type) where MkF :: Coercible f f' => (a -> f' b) -> F f a b id1F :: Coercible Identity f => F f a a id1F = MkF id1 id2F :: Coercible (Compose Identity Identity) f => F f b b id2F = MkF id2 }}} but we can not unify the types of `id1F` and `id2F`. Does this require quantified class constraints? I'm not sure where they would go -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14317> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 10

[GHC] #12152: panic: Loading temp shared object failed
by GHC 03 Jun '18

03 Jun '18

#12152: panic: Loading temp shared object failed -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 (Linking) | Keywords: | Operating System: Linux Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I've attached a no-Haskell-code project that fails when I run `cabal repl` with the following: {{{ ghc: panic! (the 'impossible' happened) (GHC version 7.10.3 for x86_64-unknown-linux): Loading temp shared object failed: /tmp/ghc60744_0/libghc_1.so: undefined symbol: _ZN2Zq1qE }}} Building the project works fine, so the problem seems to be (only) with dynamic linking. The issue can be resolved by swapping the order of the .cpp files in the cabal file. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12152> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 14

[GHC] #14546: -Woverlapping-patterns warns on wrong patterns for Int
by GHC 03 Jun '18

03 Jun '18

#14546: -Woverlapping-patterns warns on wrong patterns for Int -------------------------------------+------------------------------------- Reporter: Lemming | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC-8.0 introduced a new warning on redundant pattern matches in `case` clauses. But there is something strange. {{{ $ cat RedundantCase.hs main :: IO () main = do case 0::Int of 0 -> putStrLn "A" 1 -> putStrLn "B" _ -> putStrLn "C" case 0::Int of 0 -> putStrLn "A" 1 -> putStrLn "B" 2 -> putStrLn "C" case 0::Integer of 0 -> putStrLn "A" 1 -> putStrLn "B" _ -> putStrLn "C" case 0::Integer of 0 -> putStrLn "A" 1 -> putStrLn "B" 2 -> putStrLn "C" case 0::Integer of 1 -> putStrLn "B" 2 -> putStrLn "C" let dummy :: Integer dummy = 0 case dummy of 0 -> putStrLn "A" 1 -> putStrLn "B" _ -> putStrLn "C" case "foo" of "foo" -> putStrLn "A" "bar" -> putStrLn "B" "baz" -> putStrLn "C" if True then putStrLn "X" else putStrLn "Y" }}} {{{ $ ghc-8.2.2 -Wall RedundantCase.hs [1 of 1] Compiling Main ( RedundantCase.hs, RedundantCase.o ) RedundantCase.hs:4:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 0 -> ... | 4 | 0 -> putStrLn "A" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:5:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 1 -> ... | 5 | 1 -> putStrLn "B" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:8:4: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: 0 | 8 | case 0::Int of | ^^^^^^^^^^^^^^... RedundantCase.hs:9:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 0 -> ... | 9 | 0 -> putStrLn "A" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:10:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 1 -> ... | 10 | 1 -> putStrLn "B" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:11:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... | 11 | 2 -> putStrLn "C" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:15:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 1 -> ... | 15 | 1 -> putStrLn "B" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:16:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: _ -> ... | 16 | _ -> putStrLn "C" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:20:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 1 -> ... | 20 | 1 -> putStrLn "B" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:21:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... | 21 | 2 -> putStrLn "C" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:23:4: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: 0 | 23 | case 0::Integer of | ^^^^^^^^^^^^^^^^^^... RedundantCase.hs:24:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 1 -> ... | 24 | 1 -> putStrLn "B" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:25:7: warning: [-Woverlapping-patterns] Pattern match is redundant In a case alternative: 2 -> ... | 25 | 2 -> putStrLn "C" | ^^^^^^^^^^^^^^^^^ RedundantCase.hs:34:4: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: [] (p:_) where p is not one of {'b', 'f'} ['b'] ('b':p:_) where p is not one of {'a'} ... | 34 | case "foo" of | ^^^^^^^^^^^^^... Linking RedundantCase ... }}} In the first case it warns about the wrong patterns, in the second case it warns about all patterns and a non-exhaustive pattern list. In the following three cases using `Integer` the warnings seem to be correct. The next case shows that I can suppress the warning if I hide the constant nature of the case selector a bit. Then a case on a `String` - GHC does not seem to try to detect redundant pattern matches but falls back to a general test on exhaustive pattern lists. Finally, in a constant `case` on `Bool` I can avoid the warning using a plain `if-then-else`. Now I wonder what the purpose of the warning is at all. First I thought that it wants to warn me, that the patterns overlap, i.e. pattern `_` contains the already handled case `0`. This does not seem to be the purpose of the warning - and such overlapping patterns are pretty common, aren't they? Second thought: GHC wants to warn me about redundant patterns in the presence of a constant case selector. But then, it does so with varying degrees of success: For `Integer` it works, but not for `Int` or `String`. Is it really only about constant case selectors? Then, not only some pattern matches are redundant but the whole `case` clause is redundant. Then again, can't we assume that the programmer wrote such a `case` clause by intend? At least, this is how I use a `case` clause with constant selector: as a type-safe way to out-comment alternative implementations. Thus my question: Where is this warning useful? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14546> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 8

[GHC] #9247: Document -XDatatypeContexts in flag reference
by GHC 03 Jun '18

03 Jun '18

#9247: Document -XDatatypeContexts in flag reference ------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: low | Milestone: Component: Documentation | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- It may be a deprecated feature, but it still exists and should be listed. I can do this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9247> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 2

[GHC] #11066: Inacessible branch should be warning - otherwise breaks type soundness?
by GHC 03 Jun '18

03 Jun '18

#11066: Inacessible branch should be warning - otherwise breaks type soundness? -------------------------------------+------------------------------------- Reporter: rrnewton | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.10.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC 7.10.2 reports inaccessible branches as a type error, and I think this is really a bug. First, the implicit thinking seems to be "why would a user want to write inaccessible cases, they'd be crazy!". But that only applies to human-written code. Program generators can have a great deal of trouble avoiding this error, unless they replicate the GHC type checker to predict the problem and prune branches. (That's why we are hitting this error and are stuck.) Second, it seems like this is a problem for type soundness. See the attached program where "step1" typechecks but "step2" does not. And yet, the operational semantics should allow step1 to reduce to step2. Indeed, in the "GADTs meet their match" paper it seems like the intent was to warn for these inaccessible cases, not error. For example, the paper contains the language: "If we warn that a right-hand side of a non-redundant clause is inaccessible," -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11066> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

1 50