Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#9380 closed bug (fixed)

ghc generates seemingly incorrect code

Reported by: qnikst Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.3
Keywords: Cc: slyfox
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case: gadt/T9380
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC generates a wrong code for the case-match on GADT with polymorphic type,

here is a minimal example attached, expected results are 'A' in all test cases (this is case for ghc-HEAD), however in: test0 - result is missing as matches are removed from code (according to core) test1 - returns A as expected test2 - output 'o_O' without any checks

Attachments (1)

min.hs (1.3 KB) - added by qnikst 5 years ago.
Minimal example

Download all attachments as: .zip

Change History (9)

Changed 5 years ago by qnikst

Attachment: min.hs added

Minimal example

comment:1 Changed 5 years ago by goldfire

Status: newinfoneeded

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?

comment:2 Changed 5 years ago by qnikst

There are few reasons for this report:

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

comment:3 Changed 5 years ago by slyfox

Cc: slyfox added

comment:4 Changed 5 years ago by simonpj

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), 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

comment:5 Changed 5 years ago by simonpj

Resolution: fixed
Status: infoneededclosed
Test Case: gadt/T9380

comment:6 Changed 5 years ago by maxtaldykin

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.

comment:7 Changed 5 years ago by simonpj

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

comment:8 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

Note: See TracTickets for help on using tickets.