Implemented a preliminary subsumption check
Implemented a preliminary subsumption check

Some current examples:

>> :t x -> x
forall (a : *). a -> a

>> :t f x -> f x
forall (a : *) (b : *). (a -> b) -> a -> b

>> :t f (E x) -> f x
(interactive):1:1: error: escaped skolem

>> :t (f : some b. forall a. a -> b) (E x) -> f x
forall (a : *). (forall (b : *). b -> a) -> E -> a

>> :t ((f : some b. forall a. a -> b) (E x) -> f x) (x -> 5)
E -> Int

>> :core ((f : some b. forall a. a -> b) (E x) -> f x) (x -> 5)
(\{a,b} -> case b of c
  { <0| d> -> a d
  }) (\{a} -> 5)

ekmett/ermine,PipocaQuemada/ermine