type checker fails to reject inline annotations

[samuela]

data Lyst:
  | ly-empty
end

ly-empty :: List
ly-empty :: argchasdfasflkjfaslkjaSDFASDFASDFASDHGkasdf

passes the type checker.

[mkolosick]

This doesn't seem to reach the type checker. I ran node build/phase1/main-wrapper.js src/scripts/show-compilation.arr -type-check temp.arr.

The

ly-empty :: List
ly-empty :: argchasdfasflkjfaslkjaSDFASDFASDFASDHGkasdf

Is being removed before type-checking. Here's the program after being fully desugared:

type-let  type Lyst15 as Lyst13:
  letrec
      Lyst14 = data-expr Lyst,Lyst13: | ly-empty end,
      Lyst16 = ~Lyst14.Lyst,
      is-Lyst17 = ~Lyst14.Lyst,
      is-ly-empty18 = ~Lyst14.is-ly-empty,
      ly-empty19 = ~Lyst14.ly-empty:
    Module(Answer : nothing,
    DefinedValues :
      [ly-empty : ~ly-empty19, is-ly-empty : ~is-ly-empty18,
      is-Lyst : ~is-Lyst17, Lyst : ~Lyst16], DefinedTypes : [Lyst :: Lyst15],
    Provides : {}, Types : [], checks : builtins.current-checker().results())
  end
end

[sorawee]

See also: https://github.com/brownplt/pyret-lang/issues/529

[blerner]

This seems to be a non-issue, now that annotations are woven into the program properly. We detect that the annotations are not applied to functions, so the program gets rejected even before it gets type-checked.