3 ms·
You haven't tested the type you wrote. `type AddTest = (2 + 2) ~ 5` compiles without error the same way `addTest = (2 + 2) == 5` would run without error. To t
by tome 5y ago
You haven't tested the type you wrote. `type AddTest = (2 + 2) ~ 5` compiles without error the same way `addTest = (2 + 2) == 5` would run without error.
To test it, try, for example
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators, ConstraintKinds, TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
import GHC.TypeLits
test :: ((2 + 2) ~ 5 => a) -> a
test x = x
main = putStrLn "Hello, World!"
That will fail to compile. If you change the 5 to 4 then it will compile.
- dmitriid 5y agoThank you! This leaves only the question of cost vs benefits of these approaches :)
- whateveracct 5y agomaybe a type Test (c :: Constraint) = c => () is in order here ;) testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = ()
- tome 5y agoThat compiles though. You need to CPS the constraint as in my example above. This does the job: type Test (c :: Constraint) = forall a. (c => a) -> a testTheObvious :: Test ((2 + 2) ~ 5) testTheObvious = id