The original expression is ill typed because, as you say, the type of the body 
of the alternative mentions the existentially-bound type varaible. Core Lint 
should jolly well reject it.  (Maybe, though, it doesn't test for this?)

In Haskell it would look like this

data T where
  MkT :: forall a . a -> T

f (MKT x) = x

This is illegal.

So if GHC is producing this program, please file a ticket

Simon

From: [email protected] [mailto:[email protected]] On 
Behalf Of Andrew Farmer
Sent: 13 June 2013 04:20
To: [email protected]
Subject: exprType and existentials

Calling `exprType` on:

case enumFromStepN
       Int
       $fNumInt
       (I# 1)
       (I# 1)
       x of wild
  Stream s1 ostep t ds1 -> Left s1 ((Int, (Int, Int)), s1) t

gives:

Either s1 ((Int, (Int, Int)), s1)

Which is problematic, as the type variable 's1' is unbound outside of the 
alternative RHS!

Unfolding the scrutinee and case-reducing gives:

Left (Int, Int) ((Int, (Int, Int)), (Int, Int))
  ((,)
     Int
     Int
     (I# 1)
     (case x of n1
        I# ipv ? n1))

Calling `exprType` now gives:

Either (Int, Int) ((Int, (Int, Int)), (Int, Int))

That is, `s1` was `(Int, Int)` in this case.

Is it expected that `exprType` behaves this way? Or should I file a ticket?

I realize the type of the scrutinee (in this case Stream Int) gives no 
indication as to the existential type... and I'm not sure how you would get it 
without making exprType do some kind of evaluation, but it would be nice if 
exprType at least failed if it doesn't have enough information...

Andrew
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs

Reply via email to