Uploaded image for project: 'core.typed'
  1. CTYP-249

Propositional subtyping should consider the lexical type environment

    Details

      Description

      Problem

      Subtyping between propositions could be improved, especially when mixing positive and
      negative type propositions.

      Take the following function.

      ; Type Error (clojure/core/typed/test/core.clj:1293:14) Expected result with filter {:then (is Number a__#0), :else tt}, ; got filter {:then (! (t/U nil false) a__#0), :else (is (t/U nil false) a__#0)}
      ; in: a              |
      ;                    v
          (is-tc-e (fn [a] a)
                   [(U nil Number) -> Any :filters {:then (is Number 0)}])
      
      
      

      The subtyping test for the

      {then}

      proposition fails because

      (! (U nil false) a)
      

      is not a subtype of

      (is Number a)
      

      However in the context of the current lexical environment,

      {a (U nil Number)}
      

      combined with the actual then proposition

      (! (U nil false) a)
      

      implies

      (is Number a)
      

      .

      Approach

      Every

      {FilterSet}

      should also carry the

      {PropEnv}

      in which it was created. (We should take care that this
      environment is substituted properly when we eg. substitute function parameters for de Bruijn indices).

      Then we can check to see if the contained environment for the actual proposition set satisfies the
      supertype proposition.

      Test case:

          (is-tc-e (fn [a] a)
                   [(U nil Number) -> Any :filters {:then (is Number 0)}])
      

      Notes

      This test case should pass: let-filter-unscoping-test.

      Code review:
      Patch:

        Attachments

          Activity

            People

            • Assignee:
              ambrosebs Ambrose BS
              Reporter:
              ambrosebs Ambrose BS
            • Votes:
              0 Vote for this issue
              Watchers:
              0 Start watching this issue

              Dates

              • Created:
                Updated:
                Resolved: