Compile-time calculation for type family Min ,Max, (++), Take etc. about constraints HOT 2 CLOSED

@SkorikGG: I don't think Data.Constraint.Nat is ever going to support that. The magic in that module relies on a reflection-style trick at the value level to witness certain constraints, so you're only ever be able to use the axioms in Data.Constraint.Nat by pattern-matching against those witnesses.

That being said, you can do what you seek (a type-level Min calculation) with the ghc-typelits-extra package. For example:

$ ghci -fplugin GHC.TypeLits.Extra.Solver -XDataKinds
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :m + Data.Proxy GHC.TypeLits.Extra
λ> :t (Proxy::Proxy (Min 1 2))
(Proxy::Proxy (Min 1 2)) :: Proxy 1

from constraints.

Unfortunately, this is out of scope for what we can offer without building a compiler plugin.

from constraints.