apparently type-safe program causes eclatant runtime type mismatch

[GoogleCodeExporter]

What steps will reproduce the problem?
1. load:
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue56-CatFak.omg>

2. observe that it typechecks and offers a prompt. Enter:
(run (compile [Push 42, Push False, Prim (ArrT BoolT IntT) (\i b->if b then
1+i else i), Print]l)) (returnIO ())

[You can get this string by "svn pg testcase <URL>"]
3. Observe this error message:
Executing IO action

Case match failure
The value: 42
doesn't match any of the patterns:
  True
  False
(Vlit 42)
prompt> 

What is the expected output? What do you see instead?
Obviously this is a big no-no! "Type-safe programs do not go wrong"...

This indicates a shortcoming in the typechecker. Either the loaded program
or the testphrase is wrongly typed, but accepted nevertheless.

Original issue reported on code.google.com by ggr...@gmail.com on 7 Mar 2008 at 11:28

[GoogleCodeExporter]

same bug is present in Nov 8 snapshot too.

Original comment by ggr...@gmail.com on 7 Mar 2008 at 11:29

[GoogleCodeExporter]

Original comment by ggr...@gmail.com on 11 Jan 2011 at 4:52

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

[GoogleCodeExporter]

Maybe this is related:

prompt> let foo (a :: Code Int) = [| run a |]
prompt> foo 'k'
[| run ('k') |] : Code Int
prompt> run (foo 'k')
Run expression:
  run ('k')
Does not evaluate to code:
   'k'

which would be issue 82.

Original comment by ggr...@gmail.com on 11 Jan 2011 at 5:25

[GoogleCodeExporter]

I bet this is another manifestation of the same issue:

<http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue56-Sum.omg>

There is something that makes the combination of type functions and unification 
unsound.

Raised prio, because this does not seem to be a remote corner case any more...

Original comment by ggr...@gmail.com on 15 Jan 2011 at 1:00

• Added labels: Priority-High
• Removed labels: Priority-Medium

[GoogleCodeExporter]

haha, 
<http://svn.berlios.de/svnroot/repos/al4nin/trunk/purgatory/Sum.omg?p=1012> 
crashes Omega!

Original comment by ggr...@gmail.com on 15 Jan 2011 at 1:18

[GoogleCodeExporter]

My impression is that the latter is an "escaping existential" that goes 
undetected, or a proper universal tyvar that is not correctly propagated back 
to the calling site.

Original comment by ggr...@gmail.com on 15 Jan 2011 at 1:20

[GoogleCodeExporter]

Here is a short example:

$ cat issue56.prg 
-- Illustrate escaping existentials with type functions

subvert :: * ~> *
{subvert Int} = a -- non-parametric
{subvert Char} = Char

data FunList a = Nil | Cons {subvert a} (FunList a) deriving List(fun)

problem = ['a',42]fun

{-

ANALYSIS:
Because the first branch of 'subvert is creating a free type variable,
which ends up in contravariant position in the 'Cons' injection of
'FunList'. This makes the type variable an existential, but Omega
currently does not notice and considers 'Cons' as parametric.

I propose that we should reject the definition of FunList. We can do
this, as type functions are closed in Omega. For open type functions
I do not see a solution, as we cannot delay the type checking of the
data definition to the time where 'Cons' is called.

Btw. It should be easy to make similar type functions properly parametric
by passing in type list which doubles as a name supply.

-}

DEMO:

$ ./omega.exe issue56.prg 
Omega Interpreter: version 1.4.7pre
Build Date: unspecified

Type ':?' for command line help.
Loading source files = ["issue56.prg"]
->Loading import issue56.prg
<-issue56.prg loaded.
prompt> problem 

['a',42]fun : FunList Int
prompt> case problem of {[i;_]fun -> chr i}

omega.exe: Value not an Int: 'a'

CRASH!

Original comment by ggr...@gmail.com on 15 Jan 2011 at 2:38

[GoogleCodeExporter]

What we must avoid is that a free type variable originating from a TyFun ends 
up in a contravariant position of a constructor function.

In the above example,

{subvert Int} = a -> Int

would be ok.

Original comment by ggr...@gmail.com on 20 Jan 2011 at 10:19