    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.Misc.Newtypes
    -- Copyright : (c) Curran McConnell
    --                 Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Demonstrates how to create symbolic newtypes with the same behaviour as
    -- their wrapped type.
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror           #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE ScopedTypeVariables        #-}

    module Documentation.SBV.Examples.Misc.Newtypes where

    import Prelude hiding (ceiling)
    import Data.SBV
    import qualified Data.SBV.Internals as SI

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    -- | A 'Metres' is a newtype wrapper around 'Integer'.
    newtype Metres = Metres Integer deriving (Num Metres
    Ord Metres
    Num Metres -> Ord Metres -> (Metres -> Rational) -> Real Metres
    Metres -> Rational
    forall a. Num a -> Ord a -> (a -> Rational) -> Real a
    $ctoRational :: Metres -> Rational
    toRational :: Metres -> Rational
    Real, Enum Metres
    Real Metres
    Real Metres
    -> Enum Metres
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> (Metres, Metres))
    -> (Metres -> Metres -> (Metres, Metres))
    -> (Metres -> Integer)
    -> Integral Metres
    Metres -> Integer
    Metres -> Metres -> (Metres, Metres)
    Metres -> Metres -> Metres
    forall a.
    Real a
    -> Enum a
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> (a, a))
    -> (a -> a -> (a, a))
    -> (a -> Integer)
    -> Integral a
    $cquot :: Metres -> Metres -> Metres
    quot :: Metres -> Metres -> Metres
    $crem :: Metres -> Metres -> Metres
    rem :: Metres -> Metres -> Metres
    $cdiv :: Metres -> Metres -> Metres
    div :: Metres -> Metres -> Metres
    $cmod :: Metres -> Metres -> Metres
    mod :: Metres -> Metres -> Metres
    $cquotRem :: Metres -> Metres -> (Metres, Metres)
    quotRem :: Metres -> Metres -> (Metres, Metres)
    $cdivMod :: Metres -> Metres -> (Metres, Metres)
    divMod :: Metres -> Metres -> (Metres, Metres)
    $ctoInteger :: Metres -> Integer
    toInteger :: Metres -> Integer
    Integral, Integer -> Metres
    Metres -> Metres
    Metres -> Metres -> Metres
    (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres)
    -> (Metres -> Metres)
    -> (Metres -> Metres)
    -> (Integer -> Metres)
    -> Num Metres
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    $c+ :: Metres -> Metres -> Metres
    + :: Metres -> Metres -> Metres
    $c- :: Metres -> Metres -> Metres
    - :: Metres -> Metres -> Metres
    $c* :: Metres -> Metres -> Metres
    * :: Metres -> Metres -> Metres
    $cnegate :: Metres -> Metres
    negate :: Metres -> Metres
    $cabs :: Metres -> Metres
    abs :: Metres -> Metres
    $csignum :: Metres -> Metres
    signum :: Metres -> Metres
    $cfromInteger :: Integer -> Metres
    fromInteger :: Integer -> Metres
    Num, Int -> Metres
    Metres -> Int
    Metres -> [Metres]
    Metres -> Metres
    Metres -> Metres -> [Metres]
    Metres -> Metres -> Metres -> [Metres]
    (Metres -> Metres)
    -> (Metres -> Metres)
    -> (Int -> Metres)
    -> (Metres -> Int)
    -> (Metres -> [Metres])
    -> (Metres -> Metres -> [Metres])
    -> (Metres -> Metres -> [Metres])
    -> (Metres -> Metres -> Metres -> [Metres])
    -> Enum Metres
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: Metres -> Metres
    succ :: Metres -> Metres
    $cpred :: Metres -> Metres
    pred :: Metres -> Metres
    $ctoEnum :: Int -> Metres
    toEnum :: Int -> Metres
    $cfromEnum :: Metres -> Int
    fromEnum :: Metres -> Int
    $cenumFrom :: Metres -> [Metres]
    enumFrom :: Metres -> [Metres]
    $cenumFromThen :: Metres -> Metres -> [Metres]
    enumFromThen :: Metres -> Metres -> [Metres]
    $cenumFromTo :: Metres -> Metres -> [Metres]
    enumFromTo :: Metres -> Metres -> [Metres]
    $cenumFromThenTo :: Metres -> Metres -> Metres -> [Metres]
    enumFromThenTo :: Metres -> Metres -> Metres -> [Metres]
    Enum, Metres -> Metres -> Bool
    (Metres -> Metres -> Bool)
    -> (Metres -> Metres -> Bool) -> Eq Metres
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Metres -> Metres -> Bool
    == :: Metres -> Metres -> Bool
    $c/= :: Metres -> Metres -> Bool
    /= :: Metres -> Metres -> Bool
    Eq, Eq Metres
    Eq Metres
    -> (Metres -> Metres -> Ordering)
    -> (Metres -> Metres -> Bool)
    -> (Metres -> Metres -> Bool)
    -> (Metres -> Metres -> Bool)
    -> (Metres -> Metres -> Bool)
    -> (Metres -> Metres -> Metres)
    -> (Metres -> Metres -> Metres)
    -> Ord Metres
    Metres -> Metres -> Bool
    Metres -> Metres -> Ordering
    Metres -> Metres -> Metres
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Metres -> Metres -> Ordering
    compare :: Metres -> Metres -> Ordering
    $c< :: Metres -> Metres -> Bool
    < :: Metres -> Metres -> Bool
    $c<= :: Metres -> Metres -> Bool
    <= :: Metres -> Metres -> Bool
    $c> :: Metres -> Metres -> Bool
    > :: Metres -> Metres -> Bool
    $c>= :: Metres -> Metres -> Bool
    >= :: Metres -> Metres -> Bool
    $cmax :: Metres -> Metres -> Metres
    max :: Metres -> Metres -> Metres
    $cmin :: Metres -> Metres -> Metres
    min :: Metres -> Metres -> Metres
    Ord)

    -- | Symbolic version of 'Metres'.
    type SMetres   = SBV Metres

    -- | To use 'Metres' symbolically, we associate it with the underlying symbolic
    -- type's kind.
    instance HasKind Metres where
       kindOf :: Metres -> Kind
    kindOf Metres
    _ = Kind
    KUnbounded

    -- | The 'SymVal' instance simply uses stock definitions. This is always
    -- possible for newtypes that simply wrap over an existing symbolic type.
    instance SymVal Metres where
       mkSymVal :: forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe String -> m (SBV Metres)
    mkSymVal = Kind -> VarContext -> Maybe String -> m (SBV Metres)
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> VarContext -> Maybe String -> m (SBV a)
    SI.genMkSymVar Kind
    KUnbounded
       literal :: Metres -> SBV Metres
    literal  = Kind -> Metres -> SBV Metres
    forall a b. Integral a => Kind -> a -> SBV b
    SI.genLiteral  Kind
    KUnbounded
       fromCV :: CV -> Metres
    fromCV   = CV -> Metres
    forall a. Integral a => CV -> a
    SI.genFromCV

    -- | Similarly, we can create another newtype, this time wrapping over 'Word16'. As an example,
    -- consider measuring the human height in centimetres? The tallest person in history,
    -- Robert Wadlow, was 272 cm. We don't need negative values, so 'Word16' is the smallest type that
    -- suits our needs.
    newtype HumanHeightInCm = HumanHeightInCm Word16 deriving (Num HumanHeightInCm
    Ord HumanHeightInCm
    Num HumanHeightInCm
    -> Ord HumanHeightInCm
    -> (HumanHeightInCm -> Rational)
    -> Real HumanHeightInCm
    HumanHeightInCm -> Rational
    forall a. Num a -> Ord a -> (a -> Rational) -> Real a
    $ctoRational :: HumanHeightInCm -> Rational
    toRational :: HumanHeightInCm -> Rational
    Real, Enum HumanHeightInCm
    Real HumanHeightInCm
    Real HumanHeightInCm
    -> Enum HumanHeightInCm
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm
        -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm))
    -> (HumanHeightInCm
        -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm))
    -> (HumanHeightInCm -> Integer)
    -> Integral HumanHeightInCm
    HumanHeightInCm -> Integer
    HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
    HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    forall a.
    Real a
    -> Enum a
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> (a, a))
    -> (a -> a -> (a, a))
    -> (a -> Integer)
    -> Integral a
    $cquot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    quot :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $crem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    rem :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $cdiv :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    div :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $cmod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    mod :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $cquotRem :: HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
    quotRem :: HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
    $cdivMod :: HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
    divMod :: HumanHeightInCm
    -> HumanHeightInCm -> (HumanHeightInCm, HumanHeightInCm)
    $ctoInteger :: HumanHeightInCm -> Integer
    toInteger :: HumanHeightInCm -> Integer
    Integral, Integer -> HumanHeightInCm
    HumanHeightInCm -> HumanHeightInCm
    HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm)
    -> (Integer -> HumanHeightInCm)
    -> Num HumanHeightInCm
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    $c+ :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    + :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $c- :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    - :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $c* :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    * :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $cnegate :: HumanHeightInCm -> HumanHeightInCm
    negate :: HumanHeightInCm -> HumanHeightInCm
    $cabs :: HumanHeightInCm -> HumanHeightInCm
    abs :: HumanHeightInCm -> HumanHeightInCm
    $csignum :: HumanHeightInCm -> HumanHeightInCm
    signum :: HumanHeightInCm -> HumanHeightInCm
    $cfromInteger :: Integer -> HumanHeightInCm
    fromInteger :: Integer -> HumanHeightInCm
    Num, Int -> HumanHeightInCm
    HumanHeightInCm -> Int
    HumanHeightInCm -> [HumanHeightInCm]
    HumanHeightInCm -> HumanHeightInCm
    HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    HumanHeightInCm
    -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    (HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm)
    -> (Int -> HumanHeightInCm)
    -> (HumanHeightInCm -> Int)
    -> (HumanHeightInCm -> [HumanHeightInCm])
    -> (HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
    -> (HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
    -> (HumanHeightInCm
        -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm])
    -> Enum HumanHeightInCm
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: HumanHeightInCm -> HumanHeightInCm
    succ :: HumanHeightInCm -> HumanHeightInCm
    $cpred :: HumanHeightInCm -> HumanHeightInCm
    pred :: HumanHeightInCm -> HumanHeightInCm
    $ctoEnum :: Int -> HumanHeightInCm
    toEnum :: Int -> HumanHeightInCm
    $cfromEnum :: HumanHeightInCm -> Int
    fromEnum :: HumanHeightInCm -> Int
    $cenumFrom :: HumanHeightInCm -> [HumanHeightInCm]
    enumFrom :: HumanHeightInCm -> [HumanHeightInCm]
    $cenumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    enumFromThen :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    $cenumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    enumFromTo :: HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    $cenumFromThenTo :: HumanHeightInCm
    -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    enumFromThenTo :: HumanHeightInCm
    -> HumanHeightInCm -> HumanHeightInCm -> [HumanHeightInCm]
    Enum, HumanHeightInCm -> HumanHeightInCm -> Bool
    (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> Eq HumanHeightInCm
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: HumanHeightInCm -> HumanHeightInCm -> Bool
    == :: HumanHeightInCm -> HumanHeightInCm -> Bool
    $c/= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    /= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    Eq, Eq HumanHeightInCm
    Eq HumanHeightInCm
    -> (HumanHeightInCm -> HumanHeightInCm -> Ordering)
    -> (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> (HumanHeightInCm -> HumanHeightInCm -> Bool)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> (HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm)
    -> Ord HumanHeightInCm
    HumanHeightInCm -> HumanHeightInCm -> Bool
    HumanHeightInCm -> HumanHeightInCm -> Ordering
    HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: HumanHeightInCm -> HumanHeightInCm -> Ordering
    compare :: HumanHeightInCm -> HumanHeightInCm -> Ordering
    $c< :: HumanHeightInCm -> HumanHeightInCm -> Bool
    < :: HumanHeightInCm -> HumanHeightInCm -> Bool
    $c<= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    <= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    $c> :: HumanHeightInCm -> HumanHeightInCm -> Bool
    > :: HumanHeightInCm -> HumanHeightInCm -> Bool
    $c>= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    >= :: HumanHeightInCm -> HumanHeightInCm -> Bool
    $cmax :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    max :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    $cmin :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    min :: HumanHeightInCm -> HumanHeightInCm -> HumanHeightInCm
    Ord)

    -- | Symbolic version of 'HumanHeightInCm'.
    type SHumanHeightInCm = SBV HumanHeightInCm

    -- | Symbolic instance simply follows the underlying type, just like 'Metres'.
    instance HasKind HumanHeightInCm where
        kindOf :: HumanHeightInCm -> Kind
    kindOf HumanHeightInCm
    _ = Bool -> Int -> Kind
    KBounded Bool
    False Int
    16

    -- | Similarly here, for the 'SymVal' instance.
    instance SymVal HumanHeightInCm where
        mkSymVal :: forall (m :: * -> *).
    MonadSymbolic m =>
    VarContext -> Maybe String -> m SHumanHeightInCm
    mkSymVal = Kind -> VarContext -> Maybe String -> m SHumanHeightInCm
    forall (m :: * -> *) a.
    MonadSymbolic m =>
    Kind -> VarContext -> Maybe String -> m (SBV a)
    SI.genMkSymVar (Kind -> VarContext -> Maybe String -> m SHumanHeightInCm)
    -> Kind -> VarContext -> Maybe String -> m SHumanHeightInCm
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded Bool
    False Int
    16
        literal :: HumanHeightInCm -> SHumanHeightInCm
    literal  = Kind -> HumanHeightInCm -> SHumanHeightInCm
    forall a b. Integral a => Kind -> a -> SBV b
    SI.genLiteral  (Kind -> HumanHeightInCm -> SHumanHeightInCm)
    -> Kind -> HumanHeightInCm -> SHumanHeightInCm
    forall a b. (a -> b) -> a -> b
    $ Bool -> Int -> Kind
    KBounded Bool
    False Int
    16
        fromCV :: CV -> HumanHeightInCm
    fromCV   = CV -> HumanHeightInCm
    forall a. Integral a => CV -> a
    SI.genFromCV

    -- | The tallest human ever was 272 cm. We can simply use 'literal' to lift it
    -- to the symbolic space.
    tallestHumanEver :: SHumanHeightInCm
    tallestHumanEver :: SHumanHeightInCm
    tallestHumanEver = HumanHeightInCm -> SHumanHeightInCm
    forall a. SymVal a => a -> SBV a
    literal HumanHeightInCm
    272

    -- | Given a distance between a floor and a ceiling, we can see whether
    -- the human can stand in that room. Comparison is expressed using 'sFromIntegral'.
    ceilingHighEnoughForHuman :: SMetres -> SHumanHeightInCm -> SBool
    ceilingHighEnoughForHuman :: SBV Metres -> SHumanHeightInCm -> SBool
    ceilingHighEnoughForHuman SBV Metres
    ceiling SHumanHeightInCm
    humanHeight = SInteger
    humanHeight' SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< SInteger
    ceiling'
        where -- In a real codebase, the code for comparing these newtypes
              -- should be reusable, perhaps through a typeclass.
            ceiling' :: SInteger
    ceiling'     = Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    100 SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    * SBV Metres -> SInteger
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SBV Metres
    ceiling :: SInteger
            humanHeight' :: SInteger
    humanHeight' = SHumanHeightInCm -> SInteger
    forall a b.
    (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
     SymVal b) =>
    SBV a -> SBV b
    sFromIntegral SHumanHeightInCm
    humanHeight :: SInteger

    -- | Now, suppose we want to see whether we could design a room with a ceiling
    -- high enough that any human could stand in it. We have:
    --
    -- >>> sat problem
    -- Satisfiable. Model:
    --   floorToCeiling =   3 :: Integer
    --   humanheight    = 255 :: Word16
    problem :: Predicate
    problem :: Predicate
    problem = do
        SBV Metres
    ceiling     :: SMetres          <- String -> Symbolic (SBV Metres)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "floorToCeiling"
        SHumanHeightInCm
    humanHeight :: SHumanHeightInCm <- String -> Symbolic SHumanHeightInCm
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "humanheight"
        SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SHumanHeightInCm
    humanHeight SHumanHeightInCm -> SHumanHeightInCm -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SHumanHeightInCm
    tallestHumanEver

        SBool -> Predicate
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ SBV Metres -> SHumanHeightInCm -> SBool
    ceilingHighEnoughForHuman SBV Metres
    ceiling SHumanHeightInCm
    humanHeight