program fails to type-check

[shriram]

I can't understand why this program doesn't type-check:

import lists as L
import equality as EQ

fun sh(t :: Number, seen :: List<Number>) -> EQ.EqualityResult:
  L.member-with(seen, t, identical3)
end

The program runs without error: eg,

check:
  sh(2, [list: 1, 2, 3]) is EQ.Equal
  sh(1, empty) satisfies EQ.is-NotEqual
  sh(1, [list: 2, 3, 4]) satisfies EQ.is-NotEqual
end

but the type-checker says that the Number constraint on seen inside the function is inconsistent with the Any constraint on identical3. I thought this was just because identical3 had not been given a type, but that's not true: here's a simple program that type-checks fine

identical3(1, 2)

and another that also exercises the return type:

import equality as EQ

fun iseq<T>(v1 :: T, v2 :: T) -> String:
  cases (EQ.EqualityResult) identical3(v1, v2):
    | Equal => "yes"
    | NotEqual(_, _, _) => "no"
    | Unknown(_, _, _) => "¯\\_(ツ)_/¯"
  end
end

check:
  iseq(1, 1) is "yes"
  iseq(1, 2) is "no"
  iseq(~1, ~1) is "¯\\_(ツ)_/¯"
end

so that can't really be it…

[jpolitz]

Also, this version type-checks:

import lists as L
import equality as EQ

fun instantiate-please<A>(x :: A, y :: A) -> EQ.EqualityResult: identical3(x, y) end

fun sh(t :: Number, seen :: List<Number>) -> EQ.EqualityResult:
  L.member-with(seen, t, instantiate-please)
end

so it seems like something odd in comparing instantiated type variables with Any in constraints.