ghc generates seemingly incorrect code

changed weight to 5

Attached file min.hs ($1006).

Minimal example

As you note, this is working in HEAD. Is this ticket a request to make sure that the fix goes into 7.8.4, if that were to exist?

There are few reasons for this report:

Verify that this is a really wrong behaviour
Make sure that fix will go into 7.8.4 if it will ever be
Understand if it worth adding a regression test for the HEAD, in order track that behaviour will be correct.

I think I know what is going on. Consider test0:

test0 = let s = cast A (SomeS (S 0))
        in case viewV0 s of
	       V0A{} -> putStrLn "test0 - A"
	       V0B{} -> putStrLn "test0 - B"

Remember that cast :: forall a. M -> SomeS -> S a, so that s is a polymorphic value: s :: forall (x::M). S x.

Now at the occurrence of s on the next line, GHC has to choose what type to instantiate s at; that is, what to instantiate x with. The calling context is no help, so GHC simply has to guess any old type, of kind M. It could randomly choose A or B, but that seems arbitrary. So it chooses Any M, where Any :: forall k. k is a built-in type family that has no equations. It's as if it was declared with

type family Any :: k

So now (viewV0 s) has type V0 (Any M).

The trouble is that in GHC 7.8, Any was a data type not a type family. That was wrong for many reasons, but this ticket exposes a new one. In a case expression, GHC discards any patterns that can't possibly match the scrutinee. The two patterns in the case expression in test0 have types V0 A and V0 B. Since A and Any M are different (if Any is a data type) GHC discarded that alternative, and the same for the other one.

In HEAD, Any is a type family (see #9097 (closed)), so GHC (rightly) does not know that Any M and A are distinct. So the alternative is not discarded.

I have not followed through all the other cases, but I bet that it's all attributable to that one fix.

I will add this as regression test, despite the unsavoury use of unsafeCoerce.

I don't propose to fix 7.8.4. I think there were various reasons that Any was not made a type family earlier.

Simon

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	→ gadt/T9380

Here is a bit more concise test case (derived from the original one):

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}

import Unsafe.Coerce

data X = A | B
data Y (x :: X) where
  YA   :: Y A
  YB   :: Y B
  Yany :: String -> Y x

view :: Y a -> Y b
view = unsafeCoerce

main :: IO ()
main = case view YA of
  YA     -> putStrLn "YA"
  YB     -> putStrLn "YB"
  Yany x -> putStrLn x

This will cause segmentation fault on 7.8.3 due to matching YA with Yany and trying to access String that does not exist.

In HEAD it will print YA. But is it really intended behavior?

My reasoning is that this is an example of unsafe using of unsafeCoerce. Due to view's parametricity GHC can infer that all valid implementations (except |) are of the form

view :: Y a -> Y b
view = const (Yany "some string here")

And it is safe to optimize main by dropping YA and YB cases.

But if we allow such usage of unsafeCoerce then it is no longer possible to optimize cases even if view absolutely safe.

I think HEAD is fine here. The call view YA gets type Y (Any X), and that's a very reasonable type for it.

I don't see a difficulty here.

Simon

mentioned in commit dc7d3c2d

mentioned in issue #9429

added incorrect runtime result label

added Pnormal label

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

ghc generates seemingly incorrect code

Child items 0

Activity