[clean-list] Serious bug in the type system

[Edsko de Vries]

Hi,

I was working on the background section to my thesis and was exploring how the
single-threaded polymorphic lambda calculus deals with strict application, and
how this cannot really be properly dealt with in uniquenes typing or linear
logic (we need some hacks to make it work). This got me thinking about exactly
which hacks we need, and it turns out that the mechanism that is used in Clean
is not good enough! The following program is referentially opaque (not
referentially transparent) *but passes the typechecker*:

  module t

  import StdEnv

  ohoh :: *{#Char} -> *(*{#Char}, {#Char})
  ohoh arr
      #! arr` = arr
      = (update arr 0 'a', arr`)
  
  Start = ohoh {'x', 'y', 'z'}

The output of this program is

  ("ayz", "ayz")

Edsko