    {-# LANGUAGE BlockArguments  #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ViewPatterns    #-}
    {-# LANGUAGE Safe    #-}

    -- | Checking and conversion of 'Type's to 'FFIType's.
    module Cryptol.TypeCheck.FFI
      ( toFFIFunType
      ) where

    import           Data.Bifunctor
    import           Data.Containers.ListUtils
    import           Data.Either

    import           Cryptol.TypeCheck.FFI.Error
    import           Cryptol.TypeCheck.FFI.FFIType
    import           Cryptol.TypeCheck.SimpType
    import           Cryptol.TypeCheck.Type
    import           Cryptol.Utils.RecordMap
    import           Cryptol.Utils.Types

    -- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be
    -- satisfied for the 'FFIFunType' to be valid.
    toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
    toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
    toFFIFunType (Forall [TParam]
    params [Prop]
    _ Prop
    t) =
      -- Remove all type synonyms and simplify the type before processing it
      case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    go (Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType)))
    -> Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    forall a b. (a -> b) -> a -> b
    $ Bool -> Prop -> Prop
    tRebuild' Bool
    False Prop
    t of
        Just (Right ([Prop]
    props, FFIFunType
    fft)) -> ([Prop], FFIFunType) -> Either FFITypeError ([Prop], FFIFunType)
    forall a b. b -> Either a b
    Right
          -- Remove duplicate constraints
          ([Prop] -> [Prop]
    forall a. Ord a => [a] -> [a]
    nubOrd ([Prop] -> [Prop]) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> a -> b
    $ (TParam -> Prop) -> [TParam] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Prop -> Prop
    fin (Prop -> Prop) -> (TParam -> Prop) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TVar -> Prop
    TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    TVBound) [TParam]
    params [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    props, FFIFunType
    fft)
        Just (Left [FFITypeError]
    errs) -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIFunType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t (FFITypeErrorReason -> FFITypeError)
    -> FFITypeErrorReason -> FFITypeError
    forall a b. (a -> b) -> a -> b
    $ [FFITypeError] -> FFITypeErrorReason
    FFIBadComponentTypes [FFITypeError]
    errs
        Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    Nothing -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIFunType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIFunType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t FFITypeErrorReason
    FFINotFunction
      where go :: Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    go (TCon (TC TC
    TCFun) [Prop
    argType, Prop
    retType]) = Either [FFITypeError] ([Prop], FFIFunType)
    -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    forall a. a -> Maybe a
    Just
              case Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType Prop
    argType of
                Right ([Prop]
    ps, FFIType
    ffiArgType) ->
                  case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    go Prop
    retType of
                    Just (Right ([Prop]
    ps', FFIFunType
    ffiFunType)) -> ([Prop], FFIFunType) -> Either [FFITypeError] ([Prop], FFIFunType)
    forall a b. b -> Either a b
    Right
                      ( [Prop]
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ps'
                      , FFIFunType
    ffiFunType
                          { ffiArgTypes :: [FFIType]
    ffiArgTypes = FFIType
    ffiArgType FFIType -> [FFIType] -> [FFIType]
    forall a. a -> [a] -> [a]
    : FFIFunType -> [FFIType]
    ffiArgTypes FFIFunType
    ffiFunType } )
                    Just (Left [FFITypeError]
    errs) -> [FFITypeError] -> Either [FFITypeError] ([Prop], FFIFunType)
    forall a b. a -> Either a b
    Left [FFITypeError]
    errs
                    Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    Nothing ->
                      case Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType Prop
    retType of
                        Right ([Prop]
    ps', FFIType
    ffiRetType) -> ([Prop], FFIFunType) -> Either [FFITypeError] ([Prop], FFIFunType)
    forall a b. b -> Either a b
    Right
                          ( [Prop]
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ps'
                          , FFIFunType
                              { ffiTParams :: [TParam]
    ffiTParams = [TParam]
    params
                              , ffiArgTypes :: [FFIType]
    ffiArgTypes = [FFIType
    ffiArgType], FFIType
    ffiRetType :: FFIType
    ffiRetType :: FFIType
    .. } )
                        Left FFITypeError
    err -> [FFITypeError] -> Either [FFITypeError] ([Prop], FFIFunType)
    forall a b. a -> Either a b
    Left [FFITypeError
    err]
                Left FFITypeError
    err -> [FFITypeError] -> Either [FFITypeError] ([Prop], FFIFunType)
    forall a b. a -> Either a b
    Left
                  case Prop -> Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    go Prop
    retType of
                    Just (Right ([Prop], FFIFunType)
    _) -> [FFITypeError
    err]
                    Just (Left [FFITypeError]
    errs) -> FFITypeError
    err FFITypeError -> [FFITypeError] -> [FFITypeError]
    forall a. a -> [a] -> [a]
    : [FFITypeError]
    errs
                    Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    Nothing ->
                      case Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType Prop
    retType of
                        Right ([Prop], FFIType)
    _   -> [FFITypeError
    err]
                        Left FFITypeError
    err' -> [FFITypeError
    err, FFITypeError
    err']
            go Prop
    _ = Maybe (Either [FFITypeError] ([Prop], FFIFunType))
    forall a. Maybe a
    Nothing

    -- | Convert a 'Type' to a 'FFIType', along with any 'Prop's that must be
    -- satisfied for the 'FFIType' to be valid.
    toFFIType :: Type -> Either FFITypeError ([Prop], FFIType)
    toFFIType :: Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType Prop
    t =
      case Prop
    t of
        TCon (TC TC
    TCBit) [] -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
    forall a b. b -> Either a b
    Right ([], FFIType
    FFIBool)
        (Prop -> Maybe (Either FFITypeError FFIBasicType)
    toFFIBasicType -> Just Either FFITypeError FFIBasicType
    r) -> (\FFIBasicType
    fbt -> ([], FFIBasicType -> FFIType
    FFIBasic FFIBasicType
    fbt)) (FFIBasicType -> ([Prop], FFIType))
    -> Either FFITypeError FFIBasicType
    -> Either FFITypeError ([Prop], FFIType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Either FFITypeError FFIBasicType
    r
        TCon (TC TC
    TCSeq) [Prop]
    _ ->
          (\([Prop]
    szs, FFIBasicType
    fbt) -> ((Prop -> Prop) -> [Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Prop
    fin [Prop]
    szs, [Prop] -> FFIBasicType -> FFIType
    FFIArray [Prop]
    szs FFIBasicType
    fbt)) (([Prop], FFIBasicType) -> ([Prop], FFIType))
    -> Either FFITypeError ([Prop], FFIBasicType)
    -> Either FFITypeError ([Prop], FFIType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Prop -> Either FFITypeError ([Prop], FFIBasicType)
    go Prop
    t
          where go :: Prop -> Either FFITypeError ([Prop], FFIBasicType)
    go (Prop -> Maybe (Either FFITypeError FFIBasicType)
    toFFIBasicType -> Just Either FFITypeError FFIBasicType
    r) =
                  case Either FFITypeError FFIBasicType
    r of
                    Right FFIBasicType
    fbt -> ([Prop], FFIBasicType)
    -> Either FFITypeError ([Prop], FFIBasicType)
    forall a b. b -> Either a b
    Right ([], FFIBasicType
    fbt)
                    Left FFITypeError
    err  -> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIBasicType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t (FFITypeErrorReason -> FFITypeError)
    -> FFITypeErrorReason -> FFITypeError
    forall a b. (a -> b) -> a -> b
    $ [FFITypeError] -> FFITypeErrorReason
    FFIBadComponentTypes [FFITypeError
    err]
                go (TCon (TC TC
    TCSeq) [Prop
    sz, Prop
    ty]) = ([Prop] -> [Prop])
    -> ([Prop], FFIBasicType) -> ([Prop], FFIBasicType)
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (Prop
    szProp -> [Prop] -> [Prop]
    forall a. a -> [a] -> [a]
    :) (([Prop], FFIBasicType) -> ([Prop], FFIBasicType))
    -> Either FFITypeError ([Prop], FFIBasicType)
    -> Either FFITypeError ([Prop], FFIBasicType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Prop -> Either FFITypeError ([Prop], FFIBasicType)
    go Prop
    ty
                go Prop
    _ = FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIBasicType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t FFITypeErrorReason
    FFIBadArrayType
        TCon (TC (TCTuple Int
    _)) [Prop]
    ts ->
          case [Either FFITypeError ([Prop], FFIType)]
    -> ([FFITypeError], [([Prop], FFIType)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either FFITypeError ([Prop], FFIType)]
     -> ([FFITypeError], [([Prop], FFIType)]))
    -> [Either FFITypeError ([Prop], FFIType)]
    -> ([FFITypeError], [([Prop], FFIType)])
    forall a b. (a -> b) -> a -> b
    $ (Prop -> Either FFITypeError ([Prop], FFIType))
    -> [Prop] -> [Either FFITypeError ([Prop], FFIType)]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType [Prop]
    ts of
            ([], [([Prop], FFIType)] -> ([[Prop]], [FFIType])
    forall a b. [(a, b)] -> ([a], [b])
    unzip -> ([[Prop]]
    pss, [FFIType]
    fts)) -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
    forall a b. b -> Either a b
    Right ([[Prop]] -> [Prop]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Prop]]
    pss, [FFIType] -> FFIType
    FFITuple [FFIType]
    fts)
            ([FFITypeError]
    errs, [([Prop], FFIType)]
    _) -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t (FFITypeErrorReason -> FFITypeError)
    -> FFITypeErrorReason -> FFITypeError
    forall a b. (a -> b) -> a -> b
    $ [FFITypeError] -> FFITypeErrorReason
    FFIBadComponentTypes [FFITypeError]
    errs
        TRec RecordMap Ident Prop
    tMap ->
          case RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    -> Either FFITypeError (RecordMap Ident ([Prop], FFIType))
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a.
    Monad m =>
    RecordMap Ident (m a) -> m (RecordMap Ident a)
    sequence RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    resMap of
            Right RecordMap Ident ([Prop], FFIType)
    resMap' -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
    forall a b. b -> Either a b
    Right (([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType))
    -> ([Prop], FFIType) -> Either FFITypeError ([Prop], FFIType)
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident FFIType -> FFIType
    FFIRecord (RecordMap Ident FFIType -> FFIType)
    -> ([Prop], RecordMap Ident FFIType) -> ([Prop], FFIType)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
              ([Prop] -> ([Prop], FFIType) -> ([Prop], FFIType))
    -> [Prop]
    -> RecordMap Ident ([Prop], FFIType)
    -> ([Prop], RecordMap Ident FFIType)
    forall a b c k.
    (a -> b -> (a, c)) -> a -> RecordMap k b -> (a, RecordMap k c)
    recordMapAccum (\[Prop]
    ps ([Prop]
    ps', FFIType
    ft) -> ([Prop]
    ps' [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ps, FFIType
    ft)) [] RecordMap Ident ([Prop], FFIType)
    resMap'
            Left FFITypeError
    _ -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t (FFITypeErrorReason -> FFITypeError)
    -> FFITypeErrorReason -> FFITypeError
    forall a b. (a -> b) -> a -> b
    $
              [FFITypeError] -> FFITypeErrorReason
    FFIBadComponentTypes ([FFITypeError] -> FFITypeErrorReason)
    -> [FFITypeError] -> FFITypeErrorReason
    forall a b. (a -> b) -> a -> b
    $ [Either FFITypeError ([Prop], FFIType)] -> [FFITypeError]
    forall a b. [Either a b] -> [a]
    lefts ([Either FFITypeError ([Prop], FFIType)] -> [FFITypeError])
    -> [Either FFITypeError ([Prop], FFIType)] -> [FFITypeError]
    forall a b. (a -> b) -> a -> b
    $ RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    -> [Either FFITypeError ([Prop], FFIType)]
    forall a b. (Show a, Ord a) => RecordMap a b -> [b]
    displayElements RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    resMap
          where resMap :: RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    resMap = (Prop -> Either FFITypeError ([Prop], FFIType))
    -> RecordMap Ident Prop
    -> RecordMap Ident (Either FFITypeError ([Prop], FFIType))
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Prop -> Either FFITypeError ([Prop], FFIType)
    toFFIType RecordMap Ident Prop
    tMap
        Prop
    _ -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError ([Prop], FFIType))
    -> FFITypeError -> Either FFITypeError ([Prop], FFIType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t FFITypeErrorReason
    FFIBadType

    -- | Convert a 'Type' to a 'FFIBasicType', returning 'Nothing' if it isn't a
    -- basic type and 'Left' if it is but there was some other issue with it.
    toFFIBasicType :: Type -> Maybe (Either FFITypeError FFIBasicType)
    toFFIBasicType :: Prop -> Maybe (Either FFITypeError FFIBasicType)
    toFFIBasicType Prop
    t =
      case Prop
    t of
        TCon (TC TC
    TCSeq) [TCon (TC (TCNum Integer
    n)) [], TCon (TC TC
    TCBit) []]
          | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    8 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
    word FFIWordSize
    FFIWord8
          | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    16 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
    word FFIWordSize
    FFIWord16
          | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    32 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
    word FFIWordSize
    FFIWord32
          | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    64 -> FFIWordSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIWordSize -> Maybe (Either a FFIBasicType)
    word FFIWordSize
    FFIWord64
          | Bool
    otherwise -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a. a -> Maybe a
    Just (Either FFITypeError FFIBasicType
     -> Maybe (Either FFITypeError FFIBasicType))
    -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ FFITypeError -> Either FFITypeError FFIBasicType
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError FFIBasicType)
    -> FFITypeError -> Either FFITypeError FFIBasicType
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t FFITypeErrorReason
    FFIBadWordSize
          where word :: FFIWordSize -> Maybe (Either a FFIBasicType)
    word = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
    forall a. a -> Maybe a
    Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
    -> (FFIWordSize -> Either a FFIBasicType)
    -> FFIWordSize
    -> Maybe (Either a FFIBasicType)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicType -> Either a FFIBasicType
    forall a b. b -> Either a b
    Right (FFIBasicType -> Either a FFIBasicType)
    -> (FFIWordSize -> FFIBasicType)
    -> FFIWordSize
    -> Either a FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicValType -> FFIBasicType
    FFIBasicVal (FFIBasicValType -> FFIBasicType)
    -> (FFIWordSize -> FFIBasicValType) -> FFIWordSize -> FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> FFIWordSize -> FFIBasicValType
    FFIWord Integer
    n
        TCon (TC TC
    TCFloat) [TCon (TC (TCNum Integer
    e)) [], TCon (TC (TCNum Integer
    p)) []]
          | (Integer
    e, Integer
    p) (Integer, Integer) -> (Integer, Integer) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Integer, Integer)
    float32ExpPrec -> FFIFloatSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
    float FFIFloatSize
    FFIFloat32
          | (Integer
    e, Integer
    p) (Integer, Integer) -> (Integer, Integer) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Integer, Integer)
    float64ExpPrec -> FFIFloatSize -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. FFIFloatSize -> Maybe (Either a FFIBasicType)
    float FFIFloatSize
    FFIFloat64
          | Bool
    otherwise -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a. a -> Maybe a
    Just (Either FFITypeError FFIBasicType
     -> Maybe (Either FFITypeError FFIBasicType))
    -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ FFITypeError -> Either FFITypeError FFIBasicType
    forall a b. a -> Either a b
    Left (FFITypeError -> Either FFITypeError FFIBasicType)
    -> FFITypeError -> Either FFITypeError FFIBasicType
    forall a b. (a -> b) -> a -> b
    $ Prop -> FFITypeErrorReason -> FFITypeError
    FFITypeError Prop
    t FFITypeErrorReason
    FFIBadFloatSize
          where float :: FFIFloatSize -> Maybe (Either a FFIBasicType)
    float = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
    forall a. a -> Maybe a
    Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
    -> (FFIFloatSize -> Either a FFIBasicType)
    -> FFIFloatSize
    -> Maybe (Either a FFIBasicType)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicType -> Either a FFIBasicType
    forall a b. b -> Either a b
    Right (FFIBasicType -> Either a FFIBasicType)
    -> (FFIFloatSize -> FFIBasicType)
    -> FFIFloatSize
    -> Either a FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicValType -> FFIBasicType
    FFIBasicVal (FFIBasicValType -> FFIBasicType)
    -> (FFIFloatSize -> FFIBasicValType)
    -> FFIFloatSize
    -> FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> FFIFloatSize -> FFIBasicValType
    FFIFloat Integer
    e Integer
    p
        TCon (TC TC
    TCInteger) [] -> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
    integer Maybe Prop
    forall a. Maybe a
    Nothing
        TCon (TC TC
    TCIntMod) [Prop
    n] -> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
    forall {a}. Maybe Prop -> Maybe (Either a FFIBasicType)
    integer (Maybe Prop -> Maybe (Either FFITypeError FFIBasicType))
    -> Maybe Prop -> Maybe (Either FFITypeError FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ Prop -> Maybe Prop
    forall a. a -> Maybe a
    Just Prop
    n
        TCon (TC TC
    TCRational) [] -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a. a -> Maybe a
    Just (Either FFITypeError FFIBasicType
     -> Maybe (Either FFITypeError FFIBasicType))
    -> Either FFITypeError FFIBasicType
    -> Maybe (Either FFITypeError FFIBasicType)
    forall a b. (a -> b) -> a -> b
    $ FFIBasicType -> Either FFITypeError FFIBasicType
    forall a b. b -> Either a b
    Right (FFIBasicType -> Either FFITypeError FFIBasicType)
    -> FFIBasicType -> Either FFITypeError FFIBasicType
    forall a b. (a -> b) -> a -> b
    $ FFIBasicRefType -> FFIBasicType
    FFIBasicRef FFIBasicRefType
    FFIRational
        Prop
    _ -> Maybe (Either FFITypeError FFIBasicType)
    forall a. Maybe a
    Nothing
      where integer :: Maybe Prop -> Maybe (Either a FFIBasicType)
    integer = Either a FFIBasicType -> Maybe (Either a FFIBasicType)
    forall a. a -> Maybe a
    Just (Either a FFIBasicType -> Maybe (Either a FFIBasicType))
    -> (Maybe Prop -> Either a FFIBasicType)
    -> Maybe Prop
    -> Maybe (Either a FFIBasicType)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicType -> Either a FFIBasicType
    forall a b. b -> Either a b
    Right (FFIBasicType -> Either a FFIBasicType)
    -> (Maybe Prop -> FFIBasicType)
    -> Maybe Prop
    -> Either a FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FFIBasicRefType -> FFIBasicType
    FFIBasicRef (FFIBasicRefType -> FFIBasicType)
    -> (Maybe Prop -> FFIBasicRefType) -> Maybe Prop -> FFIBasicType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Prop -> FFIBasicRefType
    FFIInteger

    fin :: Type -> Prop
    fin :: Prop -> Prop
    fin Prop
    t = TCon -> [Prop] -> Prop
    TCon (PC -> TCon
    PC PC
    PFin) [Prop
    t]