subtyping optional keywords in HMaps

[claire alvis]

Is this me not understanding subtyping or is this an error in core.typed?  (version 0.3.22)

 

(ns test.core

  (:require [clojure.core.typed :as t]))

(t/defalias XYZMap

  (t/TFn [[x :variance :covariant :< Number]

          [y :variance :covariant :< Number]

          [z :variance :covariant :< Number]]

         (t/HMap :complete? true

                 :mandatory {:x x

                             :y (t/Option y)}

                 :optional {:z z})))

(t/defn x-getter

  [m :- (XYZMap Integer Integer Integer)] :- Integer

  (:x m))

(t/defn y-getter

  [m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)

  (:y m))

(t/defn z-getter

  [m :- (XYZMap Integer Integer Integer)] :- (t/Option Integer)

  (:z m))

I would expect all of these functions to be well typed, but I get an error only in the type of z-getter:

Type Error (test/core.clj:23:3) Type mismatch:

Expected: (t/Option Integer)

Actual: (t/U z nil)

in: (:z m)

ExceptionInfo Type Checker: Found 1 error  clojure.core/ex-info (core.clj:4593)

I would think the instantiation of z to Integer in the argument to z-getter would be enough to 

prove that the access returns "either an Integer or nil".

Claire

[Ambrose Bonnaire-Sergeant]

Hi Claire,

I bet the substitution of type variables doesn't work under optional entries. That would explain the existence of z in the final type error.

Please submit a ticket.

Thanks,
Ambrose