Crash with redundant forall

[GoogleCodeExporter]

Following program:

f :: ((forall x. Bool) -> Int) -> Bool -> Int                                   
f x = x

causes HEAD to crash with pattern match failure. Fix seems straightforward 
(remove @(LvVar _) in RankN.hs:1343).

Original issue reported on code.google.com by krz.gogo...@gmail.com on 7 Feb 2011 at 2:29

[GoogleCodeExporter]

This should result in an error message. Rank-N types involve 'forall's either 
in co- or contravariant positions of an arrow ('->' or '~>') but (forall x . 
Bool) does not contain an arrow.

Original comment by ggr...@gmail.com on 7 Feb 2011 at 6:26

• Changed state: Accepted
• Added labels: Priority-Low, Type-Defect, omega1.4.6

[GoogleCodeExporter]

Oops, turns out the above statement is not entirely correct as the type of runST

http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Monad-S
T.html#v:runST

is similarly structured.

Original comment by ggr...@gmail.com on 9 Feb 2011 at 12:41

[GoogleCodeExporter]

Another instance of the same crash:

kind X k = A k                                                                  

data Token :: k ~> *0 where                                                     
  Token :: forall (k :: *1) (a :: k). Token a                                   

x :: Token (A a)                                                                
x = Token :: Token (A a)

Both programs seem to work after removing the pattern at RankN:1343, so I think 
it should be safe.

Original comment by krz.gogo...@gmail.com on 29 Aug 2011 at 11:11

[GoogleCodeExporter]

Redundant foralls should be removed from the type:

(forall (a::*) (b::a) . Bool)  -----> Bool

Freeness can be checked recursively, innermost first:
  b ∊ Bool ==> ⊥
 a ∊ Bool ==> ⊥

This makes a Sigma to a Tau and all should be right

looking into this

Original comment by ggr...@gmail.com on 1 Sep 2011 at 10:33

• Changed state: Started
• Added labels: omega1.5
• Removed labels: omega1.4.6

[GoogleCodeExporter]

http://code.google.com/p/omega/source/browse/trunk/src/RankN.hs?spec=svn854&r=85
4#1343

Btw. that line is by me
 r664     ggreif       ; levelMap <- mapM (\lv@(LvVar _) -> do { new <- newLevel; return (lv, new) }) levelvars

As you can see I am not completely sure of the change, but it helps. Questions:

0) can we remove removeSyn (Infer.hs) ?
1) is (Forall (Nil(...)) a valid type?
2) how to handle the predicates in the Forall?

Original comment by ggr...@gmail.com on 1 Sep 2011 at 11:34

[GoogleCodeExporter]

fixed in r855. thanks for the detective work,

I'll try to sort out my questions above and see whether something needs to be 
done.

Original comment by ggr...@gmail.com on 3 Sep 2011 at 11:38

• Changed state: Fixed
• Added labels: Milestone-Release1.5.1

[GoogleCodeExporter]

Checked in your test as r857.

Some diagnostics show that these are LvMut objects. Still have to figure out 
why they show up and whether they are harmless or should be thrown/filtered out.

Original comment by ggr...@gmail.com on 3 Sep 2011 at 12:15

[GoogleCodeExporter]

Krz, can you tell me whether you introduced these redundant foralls manually or 
by some generation (expansion) mechanism?

Original comment by ggr...@gmail.com on 3 Sep 2011 at 1:12

[GoogleCodeExporter]

The ((forall x. Bool) -> Int) -> Bool -> Int was a coding mistake by me (in a 
much more complicated type with several variables), so I wouldn't care much. 
The Token example is useful to simulate type -> value functions (type classes), 
as in:

data Token :: k ~> *0 where
  Token :: forall (k :: *1) (a :: k). Token a

getequality :: Token a -> a -> a -> Bool
getequality (Token :: Token Int) = (==)
getequality (Token :: Token Bool) = eqBool
  where eqBool True True   = True
        eqBool False False = True
        eqBool _ _         = False

getfunctor :: Token f -> (a -> b) -> f a -> f b
getfunctor (Token :: Token []) = map
  where map _ [] = []
        map f (x:xs) = (f x):(map f xs)
getfunctor (Token :: Token Maybe) = mapMaybe
  where mapMaybe _ (Nothing) = Nothing
        mapMaybe f (Just x)  = Just (f x)

Original comment by krz.gogo...@gmail.com on 6 Sep 2011 at 10:32

[GoogleCodeExporter]

r878 adds a warning, so the user may correct the problem easily. I would like 
to hear from cases where the warning is a false positive, i.e. there is _no_ 
redundant type variables involved.

Reopening issue, as we are not done yet.

Original comment by ggr...@gmail.com on 7 Sep 2011 at 12:23

• Changed state: Started

[GoogleCodeExporter]

The warning triggers in this case (not redundant!)

prompt> Eq :: forall a b . Equal a b
warning: potentially redundant type variable in
  forall (c:*(1+dL)) (e:c:*(1+dL)) (f:c:*(1+dL)).Equal e f   -- (issue 91)

In the expression: Eq
the result type: level m . forall (l:*(1+m)) (n:l:*(1+m)).Equal n n
was not what was expected: Equal !j !g

And also here:

prompt> Eq :: forall a  . Equal a a
warning: potentially redundant type variable in
  forall (b:*(1+cL)) (d:b:*(1+cL)).Equal d d   -- (issue 91)

Eq : level g . forall ('f:*(1+g)) ('e:'f:*(1+g)).Equal 'e 'e

Original comment by ggr...@gmail.com on 9 Sep 2011 at 6:13

[GoogleCodeExporter]

this smells like issue 70

Original comment by ggr...@gmail.com on 10 Sep 2011 at 6:26

[GoogleCodeExporter]

Original comment by ggr...@gmail.com on 12 Sep 2011 at 7:38

• Added labels: Milestone-Release1.5.2
• Removed labels: Milestone-Release1.5.1