path: root/stdlib/source/test/lux/meta/type/check.lux

(.require
 [library
  [lux (.except symbol type)
   [abstract
    ["[0]" monad (.only do)]
    ["[0]" functor
     ["[1]T" \\test (.only Injection Comparison)]]
    ["[0]" apply
     ["[1]T" \\test]]
    [\\specification
     ["$[0]" monad]]]
   [control
    ["[0]" pipe]
    ["[0]" function]
    ["[0]" try]
    ["[0]" exception]]
   [data
    ["[0]" bit (.use "[1]#[0]" equivalence)]
    ["[0]" product]
    ["[0]" text (.use "[1]#[0]" equivalence)
     ["%" \\format (.only format)]]
    [collection
     ["[0]" list (.use "[1]#[0]" functor monoid)]
     ["[0]" set]]]
   [math
    ["[0]" random (.only Random) (.use "[1]#[0]" monad)]
    [number
     ["n" nat]]]
   [meta
    [macro
     ["^" pattern]]]
   [test
    ["_" property (.only Test)]]]]
 [\\library
  ["[0]" / (.only)
   ["/[1]" // (.use "[1]#[0]" equivalence)]]])

... TODO: Remove the following 3 definitions ASAP. //.type already exists...
(def short
  (Random Text)
  (random.unicode 10))

(def symbol
  (Random Symbol)
  (random.and ..short ..short))

(def (type' num_vars)
  (-> Nat (Random Type))
  (random.rec
   (function (_ again)
     (let [pairG (random.and again again)
           quantifiedG (random.and (random#in (list)) (type' (++ num_vars)))
           random_pair (random.either (random.either (random#each (|>> {.#Sum}) pairG)
                                                     (random#each (|>> {.#Product}) pairG))
                                      (random.either (random#each (|>> {.#Function}) pairG)
                                                     (random#each (|>> {.#Apply}) pairG)))
           random_id (let [random_id (random.either (random#each (|>> {.#Var}) random.nat)
                                                    (random#each (|>> {.#Ex}) random.nat))]
                       (when num_vars
                         0 random_id
                         _ (random.either (random#each (|>> (n.% num_vars) (n.* 2) ++ {.#Parameter}) random.nat)
                                          random_id)))
           random_quantified (random.either (random#each (|>> {.#UnivQ}) quantifiedG)
                                            (random#each (|>> {.#ExQ}) quantifiedG))]
       (all random.either
            (random#each (|>> {.#Nominal}) (random.and ..short (random#in (list))))
            random_pair
            random_id
            random_quantified
            (random#each (|>> {.#Named}) (random.and ..symbol (type' 0)))
            )))))

(def type
  (Random Type)
  (..type' 0))

(def (valid_type? type)
  (-> Type Bit)
  (when type
    {.#Nominal name params}
    (list.every? valid_type? params)
    
    {.#Ex id}
    true

    (^.with_template [<tag>]
      [{<tag> left right}
       (and (valid_type? left)
            (valid_type? right))])
    ([.#Sum] [.#Product] [.#Function])

    {.#Named name type'}
    (valid_type? type')

    _
    false))

(def injection
  (Injection (All (_ a) (/.Check a)))
  (of /.monad in))

(def comparison
  (Comparison (All (_ a) (/.Check a)))
  (function (_ == left right)
    (when [(/.result /.fresh_context left) (/.result /.fresh_context right)]
      [{try.#Success left} {try.#Success right}]
      (== left right)

      _
      false)))

(def polymorphism
  Test
  (all _.and
       (_.for [/.functor]
              (functorT.spec ..injection ..comparison /.functor))
       (_.for [/.apply]
              (applyT.spec ..injection ..comparison /.apply))
       (_.for [/.monad]
              ($monad.spec ..injection ..comparison /.monad))
       ))

(def (nominal_type parameters)
  (-> Nat (Random Type))
  (do random.monad
    [nominal (random.upper_cased 3)
     parameters (random.list parameters (nominal_type (-- parameters)))]
    (in {.#Nominal nominal parameters})))

(def clean_type
  (Random Type)
  (nominal_type 2))

(exception.def yolo)

(def error_handling
  Test
  (do random.monad
    [left ..clean_type
     right ..clean_type
     ex random.nat]
    (all _.and
         (do random.monad
           [expected (random.upper_cased 10)]
           (_.coverage [/.failure]
             (when (/.result /.fresh_context
                             (is (/.Check Any)
                                 (/.failure expected)))
               {try.#Success _} false
               {try.#Failure actual} (same? expected actual))))
         (do random.monad
           [expected (random.upper_cased 10)]
           (_.coverage [/.assertion]
             (and (when (/.result /.fresh_context
                                  (is (/.Check Any)
                                      (/.assertion expected true)))
                    {try.#Success _} true
                    {try.#Failure actual} false)
                  (when (/.result /.fresh_context (/.assertion expected false))
                    {try.#Success _} false
                    {try.#Failure actual} (same? expected actual)))))
         (_.coverage [/.except]
           (when (/.result /.fresh_context
                           (is (/.Check Any)
                               (/.except ..yolo [])))
             {try.#Success _} false
             {try.#Failure error} (exception.match? ..yolo error)))
         (let [scenario (is (-> (-> Text Bit) Type Type Bit)
                            (function (_ ? <left> <right>)
                              (and (|> (/.check <left> <right>)
                                       (is (/.Check Any))
                                       (/.result /.fresh_context)
                                       (pipe.when {try.#Failure error} (? error)
                                         {try.#Success _} false))
                                   (|> (/.check <right> <left>)
                                       (is (/.Check Any))
                                       (/.result /.fresh_context)
                                       (pipe.when {try.#Failure error} (? error)
                                         {try.#Success _} false)))))]
           (all _.and
                (_.coverage [/.type_check_failed]
                  (let [scenario (scenario (exception.match? /.type_check_failed))]
                    (and (scenario (Tuple left right) left)
                         (scenario (Tuple left right) (Or left right))
                         (scenario (Tuple left right) (-> left right))
                         (scenario (Tuple left right) {.#Ex ex})

                         (scenario (Or left right) left)
                         (scenario (Or left right) (-> left right))
                         (scenario (Or left right) {.#Ex ex})

                         (scenario (-> left right) left)
                         (scenario (-> left right) {.#Ex ex})

                         (scenario {.#Ex ex} left)
                         )))
                (_.coverage [/.invalid_type_application]
                  (let [scenario (scenario (text.contains? (the exception.#label /.invalid_type_application)))]
                    (scenario {.#Apply left right} left)))))
         )))

(def var
  Test
  (<| (_.for [/.Var])
      (all _.and
           (_.coverage [/.var]
             (when (/.result /.fresh_context
                             (do /.monad
                               [[var_id var_type] /.var]
                               (in (//#= var_type {.#Var var_id}))))
               {try.#Success verdict} verdict
               {try.#Failure error} false))
           (do random.monad
             [nominal (random.upper_cased 10)]
             (_.coverage [/.bind]
               (when (/.result /.fresh_context
                               (do /.monad
                                 [[var_id var_type] /.var
                                  _ (/.bind {.#Nominal nominal (list)}
                                            var_id)]
                                 (in true)))
                 {try.#Success _} true
                 {try.#Failure error} false)))
           (do random.monad
             [nominal (random.upper_cased 10)]
             (_.coverage [/.bound?]
               (and (|> (do /.monad
                          [[var_id var_type] /.var
                           pre (/.bound? var_id)
                           _ (/.bind {.#Nominal nominal (list)}
                                     var_id)
                           post (/.bound? var_id)]
                          (in (and (not pre)
                                   post)))
                        (/.result /.fresh_context)
                        (try.else false))
                    (|> (do /.monad
                          [[var_id var/0] /.var
                           pre (/.bound? var_id)
                           [_ var/1] /.var
                           _ (/.check var/0 var/1)
                           post (/.bound? var_id)]
                          (in (and (not pre)
                                   (not post))))
                        (/.result /.fresh_context)
                        (try.else false)))))
           (do random.monad
             [nominal (random.upper_cased 10)]
             (_.coverage [/.cannot_rebind_var]
               (when (/.result /.fresh_context
                               (do /.monad
                                 [[var_id var_type] /.var
                                  _ (/.bind {.#Nominal nominal (list)}
                                            var_id)]
                                 (/.bind {.#Nominal nominal (list)}
                                         var_id)))
                 {try.#Success _}
                 false
                 
                 {try.#Failure error}
                 (exception.match? /.cannot_rebind_var error))))
           (do random.monad
             [nominal (random.upper_cased 10)
              var_id random.nat]
             (_.coverage [/.unknown_type_var]
               (when (/.result /.fresh_context
                               (/.bind {.#Nominal nominal (list)}
                                       var_id))
                 {try.#Success _}
                 false
                 
                 {try.#Failure error}
                 (exception.match? /.unknown_type_var error))))
           (do random.monad
             [nominal (random.upper_cased 10)
              .let [expected {.#Nominal nominal (list)}]]
             (_.coverage [/.peek]
               (and (|> (do /.monad
                          [[var_id var_type] /.var]
                          (/.peek var_id))
                        (/.result /.fresh_context)
                        (pipe.when {try.#Success {.#None}} true
                          _ false))
                    (|> (do /.monad
                          [[var_id var/0] /.var
                           [_ var/1] /.var
                           _ (/.check var/0 var/1)]
                          (/.peek var_id))
                        (/.result /.fresh_context)
                        (pipe.when {try.#Success {.#None}} true
                          _ false))
                    (|> (do /.monad
                          [[var_id var_type] /.var
                           _ (/.bind expected var_id)]
                          (/.peek var_id))
                        (/.result /.fresh_context)
                        (pipe.when {try.#Success {.#Some actual}}
                          (same? expected actual)
                          
                          _
                          false)))))
           (do random.monad
             [nominal (random.upper_cased 10)
              .let [expected {.#Nominal nominal (list)}]]
             (_.coverage [/.read]
               (when (/.result /.fresh_context
                               (do /.monad
                                 [[var_id var_type] /.var
                                  _ (/.bind expected var_id)]
                                 (/.read var_id)))
                 {try.#Success actual}
                 (same? expected actual)
                 
                 _
                 false)))
           (do random.monad
             [nominal (random.upper_cased 10)
              .let [expected {.#Nominal nominal (list)}]]
             (_.coverage [/.unbound_type_var]
               (when (/.result /.fresh_context
                               (do /.monad
                                 [[var_id var_type] /.var]
                                 (/.read var_id)))
                 {try.#Failure error}
                 (exception.match? /.unbound_type_var error)

                 _
                 false)))
           )))

(def context
  Test
  (all _.and
       (_.coverage [/.fresh_context]
         (and (n.= 0 (the .#var_counter /.fresh_context))
              (n.= 0 (the .#ex_counter /.fresh_context))
              (list.empty? (the .#var_bindings /.fresh_context))))
       (_.coverage [/.context]
         (and (when (/.result /.fresh_context /.context)
                {try.#Success actual}
                (same? /.fresh_context actual)
                
                {try.#Failure error}
                false)
              (when (/.result /.fresh_context
                              (do /.monad
                                [_ /.var]
                                /.context))
                {try.#Success actual}
                (and (n.= 1 (the .#var_counter actual))
                     (n.= 0 (the .#ex_counter actual))
                     (n.= 1 (list.size (the .#var_bindings actual))))
                
                {try.#Failure error}
                false)))
       (_.coverage [/.existential]
         (when (/.result /.fresh_context
                         (do /.monad
                           [_ /.existential]
                           /.context))
           {try.#Success actual}
           (and (n.= 0 (the .#var_counter actual))
                (n.= 1 (the .#ex_counter actual))
                (n.= 0 (list.size (the .#var_bindings actual))))
           
           {try.#Failure error}
           false))
       ))

(def succeeds?
  (All (_ a) (-> (/.Check a) Bit))
  (|>> (/.result /.fresh_context)
       (pipe.when {try.#Success _}
         true

         {try.#Failure error}
         false)))

(def fails?
  (All (_ a) (-> (/.Check a) Bit))
  (|>> ..succeeds?
       not))

(def nominal
  (Random Type)
  (do random.monad
    [name (random.upper_cased 10)]
    (in {.#Nominal name (list)})))

(def (non_twins = random)
  (All (_ a) (-> (-> a a Bit) (Random a) (Random [a a])))
  (do random.monad
    [left random
     right (random.only (|>> (= left) not) random)]
    (in [left right])))

(.type Super
  (Ex (_ sub) [Text sub]))

(.type Sub
  (Super Bit))

(def (handles_nominal_types! name/0 name/1 parameter/0 parameter/1)
  (-> Text Text Type Type Bit)
  (let [names_matter!
        (and (..succeeds? (/.check {.#Nominal name/0 (list)}
                                   {.#Nominal name/0 (list)}))
             (..fails? (/.check {.#Nominal name/0 (list)}
                                {.#Nominal name/1 (list)})))

        parameters_matter!
        (and (..succeeds? (/.check {.#Nominal name/0 (list parameter/0)}
                                   {.#Nominal name/0 (list parameter/0)}))
             (..fails? (/.check {.#Nominal name/0 (list parameter/0)}
                                {.#Nominal name/0 (list parameter/1)})))

        covariant_parameters!
        (and (..succeeds? (/.check {.#Nominal name/0 (list Super)}
                                   {.#Nominal name/0 (list Sub)}))
             (..fails? (/.check {.#Nominal name/0 (list Sub)}
                                {.#Nominal name/0 (list Super)})))]
    (and names_matter!
         parameters_matter!
         covariant_parameters!)))

(with_template [<assertion> <combinator>]
  [(def (<assertion> name/0 name/1)
     (-> Text Text Bit)
     (let [pair/0 {<combinator> {.#Nominal name/0 (list)} {.#Nominal name/0 (list)}}
           pair/1 {<combinator> {.#Nominal name/1 (list)} {.#Nominal name/1 (list)}}
           
           invariant!
           (and (..succeeds? (/.check pair/0 pair/0))
                (..fails? (/.check pair/0 pair/1)))

           super_pair {<combinator> Super Super}
           sub_pair {<combinator> Sub Sub}
           
           covariant!
           (and (..succeeds? (/.check super_pair sub_pair))
                (..fails? (/.check sub_pair super_pair)))]
       (and invariant!
            covariant!)))]

  [handles_products! .#Product]
  [handles_sums! .#Sum]
  )

(def (handles_function_variance! nominal)
  (-> Type Bit)
  (let [functions_have_contravariant_inputs!
        (..succeeds? (/.check {.#Function Sub nominal} {.#Function Super nominal}))
        
        functions_have_covariant_outputs!
        (..succeeds? (/.check {.#Function nominal Super} {.#Function nominal Sub}))]
    (and functions_have_contravariant_inputs!
         functions_have_covariant_outputs!)))

(def (verdict check)
  (All (_ _) (-> (/.Check _) (/.Check Bit)))
  (function (_ context)
    {try.#Success [context (when (check context)
                             {try.#Success _}
                             true

                             {try.#Failure _}
                             false)]}))

(def (build_ring tail_size)
  (-> Nat (/.Check [Type (List Type) Type]))
  (do [! /.monad]
    [[id/head var/head] /.var
     var/tail+ (monad.each ! (function (_ _)
                               (do !
                                 [[id/T var/tail] /.var]
                                 (in var/tail)))
                           (list.repeated tail_size /.var))
     var/last (monad.mix ! (function (_ var/next var/prev)
                             (do !
                               [_ (/.check var/prev var/next)]
                               (in var/next)))
                         var/head
                         var/tail+)
     _ (/.check var/last var/head)]
    (in [var/head var/tail+ var/last])))

(def (handles_var_rings! tail_size nominal/0 nominal/1)
  (-> Nat Type Type Bit)
  (let [can_create_rings_of_variables!
        (succeeds? (..build_ring tail_size))

        can_bind_rings_of_variables!
        (succeeds? (do [! /.monad]
                     [[var/head var/tail+ var/last] (..build_ring tail_size)
                      _ (/.check var/head nominal/0)
                      failures (monad.each ! (|>> (/.check nominal/1) ..verdict) (list.partial var/head var/tail+))
                      successes (monad.each ! (|>> (/.check nominal/0) ..verdict) (list.partial var/head var/tail+))]
                     (/.assertion "" (and (list.every? (bit#= false) failures)
                                          (list.every? (bit#= true) successes)))))

        can_merge_multiple_rings_of_variables!
        (succeeds? (do [! /.monad]
                     [[var/head/0 var/tail+/0 var/last/0] (..build_ring tail_size)
                      [var/head/1 var/tail+/1 var/last/1] (..build_ring tail_size)
                      _ (/.check var/head/0 var/head/1)
                      _ (/.check var/head/0 nominal/0)
                      .let [all_variables (list#composite (list.partial var/head/0 var/tail+/0)
                                                          (list.partial var/head/1 var/tail+/1))]
                      failures (monad.each ! (|>> (/.check nominal/1) ..verdict) all_variables)
                      successes (monad.each ! (|>> (/.check nominal/0) ..verdict) all_variables)]
                     (/.assertion "" (and (list.every? (bit#= false) failures)
                                          (list.every? (bit#= true) successes)))))]
    (and can_create_rings_of_variables!
         can_bind_rings_of_variables!
         can_merge_multiple_rings_of_variables!)))

(def (handles_vars! nominal)
  (-> Type Bit)
  (let [vars_check_against_themselves!
        (succeeds? (do /.monad
                     [[id var] /.var]
                     (/.check var var)))

        can_bind_vars_by_checking_against_them!
        (and (succeeds? (do /.monad
                          [[id var] /.var]
                          (/.check var nominal)))
             (succeeds? (do /.monad
                          [[id var] /.var]
                          (/.check nominal var))))

        cannot_rebind!
        (fails? (do /.monad
                  [[id var] /.var
                   _ (/.check var nominal)]
                  (/.check var ..Sub)))

        bound_vars_check_against_their_bound_types!
        (and (succeeds? (do /.monad
                          [[id var] /.var
                           _ (/.check var nominal)]
                          (/.check nominal var)))
             (succeeds? (do /.monad
                          [[id var] /.var
                           _ (/.check var ..Super)]
                          (/.check var ..Sub)))
             (succeeds? (do /.monad
                          [[id var] /.var
                           _ (/.check var ..Sub)]
                          (/.check ..Super var)))

             (fails? (do /.monad
                       [[id var] /.var
                        _ (/.check var ..Super)]
                       (/.check ..Sub var)))
             (fails? (do /.monad
                       [[id var] /.var
                        _ (/.check var ..Sub)]
                       (/.check var ..Super))))]
    (and vars_check_against_themselves!
         can_bind_vars_by_checking_against_them!
         cannot_rebind!
         bound_vars_check_against_their_bound_types!)))

(def handles_existentials!
  Bit
  (let [existentials_always_match_themselves!
        (..succeeds? (do /.monad
                       [[_ single] /.existential]
                       (/.check single single)))

        existentials_never_match_each_other!
        (..fails? (do /.monad
                    [[_ left] /.existential
                     [_ right] /.existential]
                    (/.check left right)))]
    (and existentials_always_match_themselves!
         existentials_never_match_each_other!)))

(def (handles_quantification! nominal)
  (-> Type Bit)
  (let [universals_satisfy_themselves!
        (..succeeds? (/.check (.type_literal (All (_ a) (Maybe a)))
                              (.type_literal (All (_ a) (Maybe a)))))

        existentials_satisfy_themselves!
        (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a)))
                              (.type_literal (Ex (_ a) (Maybe a)))))

        universals_satisfy_particulars!
        (..succeeds? (/.check (.type_literal (Maybe nominal))
                              (.type_literal (All (_ a) (Maybe a)))))

        particulars_do_not_satisfy_universals!
        (..fails? (/.check (.type_literal (All (_ a) (Maybe a)))
                           (.type_literal (Maybe nominal))))

        particulars_satisfy_existentials!
        (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a)))
                              (.type_literal (Maybe nominal))))

        existentials_do_not_satisfy_particulars!
        (..fails? (/.check (.type_literal (Maybe nominal))
                           (.type_literal (Ex (_ a) (Maybe a)))))]
    (and universals_satisfy_themselves!
         existentials_satisfy_themselves!

         universals_satisfy_particulars!
         particulars_do_not_satisfy_universals!
         
         particulars_satisfy_existentials!
         existentials_do_not_satisfy_particulars!
         )))

(def (handles_ultimates! nominal)
  (-> Type Bit)
  (let [any_is_the_ultimate_super_type!
        (and (..succeeds? (/.check Any nominal))
             (..fails? (/.check nominal Any)))

        nothing_is_the_ultimate_sub_type!
        (and (..succeeds? (/.check nominal Nothing))
             (..fails? (/.check Nothing nominal)))

        ultimates_check_themselves!
        (and (..succeeds? (/.check Any Any))
             (..succeeds? (/.check Nothing Nothing)))]
    (and any_is_the_ultimate_super_type!
         nothing_is_the_ultimate_sub_type!
         ultimates_check_themselves!)))

(def (names_do_not_affect_types! left_name right_name nominal)
  (-> Symbol Symbol Type Bit)
  (and (..succeeds? (/.check {.#Named left_name Any} nominal))
       (..succeeds? (/.check Any {.#Named right_name nominal}))
       (..succeeds? (/.check {.#Named left_name Any} {.#Named right_name nominal}))))

... TODO: Test all the crazy corner cases from /.check_apply
(def (handles_application! nominal/0 nominal/1)
  (-> Type Type Bit)
  (let [types_flow_through!
        (and (..succeeds? (/.check (.type_literal ((All (_ a) a) nominal/0))
                                   nominal/0))
             (..succeeds? (/.check nominal/0
                                   (.type_literal ((All (_ a) a) nominal/0))))

             (..succeeds? (/.check (.type_literal ((Ex (_ a) a) nominal/0))
                                   nominal/0))
             (..succeeds? (/.check nominal/0
                                   (.type_literal ((Ex (_ a) a) nominal/0)))))

        multiple_parameters!
        (and (..succeeds? (/.check (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1))
                                   (.type_literal [nominal/0 nominal/1])))
             (..succeeds? (/.check (.type_literal [nominal/0 nominal/1])
                                   (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1))))
             
             (..succeeds? (/.check (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1))
                                   (.type_literal [nominal/0 nominal/1])))
             (..succeeds? (/.check (.type_literal [nominal/0 nominal/1])
                                   (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1)))))]
    (and types_flow_through!
         multiple_parameters!)))

(def check
  Test
  (do [! random.monad]
    [nominal ..nominal
     [name/0 name/1] (..non_twins text#= (random.upper_cased 10))
     [parameter/0 parameter/1] (..non_twins //#= ..nominal)
     left_name ..symbol
     right_name ..symbol
     ring_tail_size (of ! each (n.% 10) random.nat)]
    (_.coverage [/.check]
      (and (..handles_nominal_types! name/0 name/1 parameter/0 parameter/1)
           (..handles_products! name/0 name/1)
           (..handles_sums! name/0 name/1)
           (..handles_function_variance! nominal)
           (..handles_vars! nominal)
           (..handles_var_rings! ring_tail_size parameter/0 parameter/1)
           ..handles_existentials!
           (..handles_quantification! nominal)
           (..handles_ultimates! nominal)
           (..handles_application! parameter/0 parameter/1)
           (..names_do_not_affect_types! left_name right_name nominal)
           ))))

(def dirty_type
  (Random (-> Type Type))
  (random.rec
   (function (_ dirty_type)
     (`` (all random.either
              (random#each (function (_ id)
                             (function.constant {.#Ex id}))
                           random.nat)
              (do random.monad
                [module (random.upper_cased 10)
                 short (random.upper_cased 10)
                 anonymousT dirty_type]
                (in (function (_ holeT)
                      {.#Named [module short] (anonymousT holeT)})))
              (,, (with_template [<tag>]
                    [(do random.monad
                       [leftT dirty_type
                        rightT dirty_type]
                       (in (function (_ holeT)
                             {<tag> (leftT holeT) (rightT holeT)})))]

                    [.#Sum]
                    [.#Product]
                    [.#Function]
                    [.#Apply]
                    ))
              (do [! random.monad]
                [name (random.upper_cased 10)
                 parameterT dirty_type]
                (in (function (_ holeT)
                      {.#Nominal name (list (parameterT holeT))})))
              (,, (with_template [<tag>]
                    [(do [! random.monad]
                       [funcT dirty_type
                        argT dirty_type
                        body random.nat]
                       (in (function (_ holeT)
                             {<tag> (list (funcT holeT) (argT holeT))
                                    {.#Parameter body}})))]

                    [.#UnivQ]
                    [.#ExQ]
                    ))
              )))))

(def clean
  Test
  (do random.monad
    [type_shape ..dirty_type]
    (_.coverage [/.clean]
      (and (|> (do /.monad
                 [[var_id varT] /.var
                  cleanedT (/.clean (list) (type_shape varT))]
                 (in (//#= (type_shape varT)
                           cleanedT)))
               (/.result /.fresh_context)
               (try.else false))
           (|> (do /.monad
                 [[var_id varT] /.var
                  [_ replacementT] /.existential
                  _ (/.check varT replacementT)
                  cleanedT (/.clean (list) (type_shape varT))]
                 (in (//#= (type_shape replacementT)
                           cleanedT)))
               (/.result /.fresh_context)
               (try.else false))
           ))))

(def for_subsumption|ultimate
  (Random Bit)
  (do random.monad
    [example ..clean_type]
    (in (and (/.subsumes? .Any example)
             (not (/.subsumes? example .Any))
             
             (/.subsumes? example .Nothing)
             (not (/.subsumes? .Nothing example))
             ))))

(def for_subsumption|nominal
  (Random Bit)
  (do random.monad
    [nominal (random.upper_cased 10)
     example ..clean_type]
    (in (and (/.subsumes? {.#Nominal nominal (list)}
                          {.#Nominal nominal (list)})
             (/.subsumes? {.#Nominal nominal (list .Any)}
                          {.#Nominal nominal (list example)})
             (not (/.subsumes? {.#Nominal nominal (list example)}
                               {.#Nominal nominal (list .Any)}))
             (/.subsumes? {.#Nominal nominal (list example)}
                          {.#Nominal nominal (list .Nothing)})
             (not (/.subsumes? {.#Nominal nominal (list .Nothing)}
                               {.#Nominal nominal (list example)}))
             ))))

(def for_subsumption|sum
  (Random Bit)
  (do random.monad
    [left ..clean_type
     right ..clean_type]
    (in (and (/.subsumes? {.#Sum .Any .Any}
                          {.#Sum left right})
             (not (/.subsumes? {.#Sum left right}
                               {.#Sum .Any .Any}))
             (/.subsumes? {.#Sum left right}
                          {.#Sum .Nothing .Nothing})
             (not (/.subsumes? {.#Sum .Nothing .Nothing}
                               {.#Sum left right}))
             ))))

(def for_subsumption|product
  (Random Bit)
  (do random.monad
    [left ..clean_type
     right ..clean_type]
    (in (and (/.subsumes? {.#Product .Any .Any}
                          {.#Product left right})
             (not (/.subsumes? {.#Product left right}
                               {.#Product .Any .Any}))
             (/.subsumes? {.#Product left right}
                          {.#Product .Nothing .Nothing})
             (not (/.subsumes? {.#Product .Nothing .Nothing}
                               {.#Product left right}))
             ))))

(def for_subsumption|function
  (Random Bit)
  (do random.monad
    [left ..clean_type
     right ..clean_type]
    (in (and (/.subsumes? {.#Function .Nothing .Any}
                          {.#Function left right})
             (not (/.subsumes? {.#Function left right}
                               {.#Function .Nothing .Any}))
             (not (/.subsumes? {.#Function .Any .Nothing}
                               {.#Function left right}))
             ))))

(with_template [<tag> <name>]
  [(def <name>
     (Random Bit)
     (do random.monad
       [id random.nat
        example ..clean_type]
       (in (not (or (/.subsumes? {<tag> id} example)
                    (/.subsumes? example {<tag> id}))))))]

  [.#Var for_subsumption|variable]
  [.#Ex for_subsumption|existential]
  )

(def for_subsumption|quantification+application
  (Random Bit)
  (do random.monad
    [example ..clean_type]
    (in (and (and (/.subsumes? (.type_literal (List example)) (.type_literal (All (_ a) (List a))))
                  (not (/.subsumes? (.type_literal (All (_ a) (List a))) (.type_literal (List example)))))
             (and (/.subsumes? (.type_literal (Ex (_ a) (List a))) (.type_literal (List example)))
                  (not (/.subsumes? (.type_literal (List example)) (.type_literal (Ex (_ a) (List a))))))))))

(def for_subsumption|named
  (Random Bit)
  (do random.monad
    [module (random.upper_cased 10)
     short (random.upper_cased 10)
     example ..clean_type]
    (in (and (/.subsumes? {.#Named [module short] example}
                          example)
             (/.subsumes? example
                          {.#Named [module short] example})
             ))))

(def for_subsumption
  Test
  (do random.monad
    [for_subsumption|ultimate ..for_subsumption|ultimate
     for_subsumption|nominal ..for_subsumption|nominal
     for_subsumption|sum ..for_subsumption|sum
     for_subsumption|product ..for_subsumption|product
     for_subsumption|function ..for_subsumption|function
     for_subsumption|variable ..for_subsumption|variable
     for_subsumption|existential ..for_subsumption|existential
     for_subsumption|quantification+application ..for_subsumption|quantification+application
     for_subsumption|named ..for_subsumption|named]
    (_.coverage [/.subsumes?]
      (and for_subsumption|ultimate
           for_subsumption|nominal
           for_subsumption|sum
           for_subsumption|product
           for_subsumption|function
           for_subsumption|variable
           for_subsumption|existential
           for_subsumption|quantification+application
           for_subsumption|named
           ))))

(def .public test
  Test
  (<| (_.covering /._)
      (_.for [/.Check])
      (all _.and
           ..polymorphism
           (do random.monad
             [expected random.nat]
             (_.coverage [/.result]
               (when (/.result /.fresh_context
                               (of /.monad in expected))
                 {try.#Success actual} (same? expected actual)
                 {try.#Failure error} false)))
           ..error_handling
           ..var
           ..context
           ..check
           ..clean
           ..for_subsumption
           )))