johnynek / bosatsu

A python-ish pure and total functional programming language
Apache License 2.0
224 stars 11 forks source link

universally quantified functions fail when types are explicit #1023

Closed johnynek closed 1 year ago

johnynek commented 1 year ago

see:

https://github.com/johnynek/bosatsu/pull/1022/commits/f013d61f92234e3424d6562d2a7e65205a58048d#diff-d8d4673b7b87bb063e5886cf096e7ab343a1f277a30926bf1376c1fa9a016a54R892

package A
enum Cont[a: *]:
  Item(a: a)
  Next(use: (Cont[a] -> a) -> a)
def map[a](ca: Cont[a], fn: a -> a) -> Cont[a]:
  Next(cont -> fn(cont(ca)))
# this fails if we write loop[a]
#def loop[a](box: Cont[a]) -> a:
def loop(box: Cont[a]) -> a:
  recur box:
    case Item(a): a
    case Next(cont_fn):
      cont_fn(cont -> loop(cont))
loopgen: forall a. Cont[a] -> a = loop
b: Cont[Int] = Item(1).map(x -> x.add(1))
main: Int = loop(b)

def loop(box: Cont[a]) -> a should work exactly like def loop[a](box: Cont[a]) -> a but somehow it fails.

The latter triggers Expr.Generic being created at the outer layer, which suggests that Expr.Generic has some bugs.