Having set types like this and refining them smaller is something I wish Haskell would learn from Typescript, especially the automatic inference side. I wonder if it would help with linear types? Are there any proposals? I know there are type level naturals in the type system, but this is more like wanting to deconstruct existing types like Int or String into subset types.

e.g.,

foo :: Int -> 3::Int | 4::Int

foo 4 = 4

foo _ = 3

bar :: 3::Int | 4::Int -> Bool

bar 4 = True

bar 3 = False

-- (bar 12) is a compiler error, and no need to handle other patterns

baz :: 3::Int | 2::Int -> Bool

bar 3 = True

bar x = False -- Type of x is 2::Int