{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Unified.Internal.Class.UnifiedFromIntegral
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Unified.Internal.Class.UnifiedFromIntegral
  ( UnifiedFromIntegral (..),
    symFromIntegral,
  )
where

import Data.Type.Bool (If)
import Data.Typeable (Typeable)
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SymFromIntegral (SymFromIntegral)
import qualified Grisette.Internal.Core.Data.Class.SymFromIntegral as SymFromIntegral
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, ValidFP)
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym), IsConMode)
import Grisette.Unified.Internal.Util (withMode)

-- | Unified `Grisette.Internal.Core.Data.Class.SymFromIntegral.symFromIntegral`
-- operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > symFromIntegral @mode a
symFromIntegral ::
  forall mode a b. (Typeable mode, UnifiedFromIntegral mode a b) => a -> b
symFromIntegral :: forall (mode :: EvalModeTag) a b.
(Typeable mode, UnifiedFromIntegral mode a b) =>
a -> b
symFromIntegral a
a =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a b r.
UnifiedFromIntegral mode a b =>
(If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
 r)
-> r
withBaseFromIntegral @mode @a @b ((If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
  b)
 -> b)
-> (If
      (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
    b)
-> b
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a)
    (forall (mode :: EvalModeTag) a b r.
UnifiedFromIntegral mode a b =>
(If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
 r)
-> r
withBaseFromIntegral @mode @a @b ((If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
  b)
 -> b)
-> (If
      (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
    b)
-> b
forall a b. (a -> b) -> a -> b
$ a -> b
forall from to. SymFromIntegral from to => from -> to
SymFromIntegral.symFromIntegral a
a)

-- | A class that provides unified conversion from integral types.
--
-- We use this type class to help resolve the constraints for `SymFromIntegral`.
class UnifiedFromIntegral (mode :: EvalModeTag) a b where
  withBaseFromIntegral ::
    ((If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b)) => r) -> r

instance
  {-# INCOHERENT #-}
  ( Typeable mode,
    (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b))
  ) =>
  UnifiedFromIntegral mode a b
  where
  withBaseFromIntegral :: forall r.
(If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) =>
 r)
-> r
withBaseFromIntegral If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r
r = r
If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r
r

instance UnifiedFromIntegral 'Con Integer AlgReal where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral Integer, Num AlgReal)
   (SymFromIntegral Integer AlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral Integer, Num AlgReal)
  (SymFromIntegral Integer AlgReal) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral Integer, Num AlgReal)
  (SymFromIntegral Integer AlgReal) =>
r
r

instance UnifiedFromIntegral 'Con Integer Integer where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral Integer, Num Integer)
   (SymFromIntegral Integer Integer) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral Integer, Num Integer)
  (SymFromIntegral Integer Integer) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral Integer, Num Integer)
  (SymFromIntegral Integer Integer) =>
r
r

instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (IntN n) where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral Integer, Num (IntN n))
   (SymFromIntegral Integer (IntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral Integer, Num (IntN n))
  (SymFromIntegral Integer (IntN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral Integer, Num (IntN n))
  (SymFromIntegral Integer (IntN n)) =>
r
r

instance
  (KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Con Integer (WordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral Integer, Num (WordN n))
   (SymFromIntegral Integer (WordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral Integer, Num (WordN n))
  (SymFromIntegral Integer (WordN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral Integer, Num (WordN n))
  (SymFromIntegral Integer (WordN n)) =>
r
r

instance (ValidFP eb sb) => UnifiedFromIntegral 'Con Integer (FP eb sb) where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral Integer, Num (FP eb sb))
   (SymFromIntegral Integer (FP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral Integer, Num (FP eb sb))
  (SymFromIntegral Integer (FP eb sb)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral Integer, Num (FP eb sb))
  (SymFromIntegral Integer (FP eb sb)) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Con (IntN n') AlgReal
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (IntN n'), Num AlgReal)
   (SymFromIntegral (IntN n') AlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (IntN n'), Num AlgReal)
  (SymFromIntegral (IntN n') AlgReal) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (IntN n'), Num AlgReal)
  (SymFromIntegral (IntN n') AlgReal) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Con (IntN n') Integer
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (IntN n'), Num Integer)
   (SymFromIntegral (IntN n') Integer) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (IntN n'), Num Integer)
  (SymFromIntegral (IntN n') Integer) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (IntN n'), Num Integer)
  (SymFromIntegral (IntN n') Integer) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Con (IntN n') (IntN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (IntN n'), Num (IntN n))
   (SymFromIntegral (IntN n') (IntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (IntN n))
  (SymFromIntegral (IntN n') (IntN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (IntN n))
  (SymFromIntegral (IntN n') (IntN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Con (IntN n') (WordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (IntN n'), Num (WordN n))
   (SymFromIntegral (IntN n') (WordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (WordN n))
  (SymFromIntegral (IntN n') (WordN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (WordN n))
  (SymFromIntegral (IntN n') (WordN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'Con (IntN n') (FP eb sb)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (IntN n'), Num (FP eb sb))
   (SymFromIntegral (IntN n') (FP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (FP eb sb))
  (SymFromIntegral (IntN n') (FP eb sb)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (IntN n'), Num (FP eb sb))
  (SymFromIntegral (IntN n') (FP eb sb)) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Con (WordN n') AlgReal
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (WordN n'), Num AlgReal)
   (SymFromIntegral (WordN n') AlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (WordN n'), Num AlgReal)
  (SymFromIntegral (WordN n') AlgReal) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (WordN n'), Num AlgReal)
  (SymFromIntegral (WordN n') AlgReal) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Con (WordN n') Integer
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (WordN n'), Num Integer)
   (SymFromIntegral (WordN n') Integer) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (WordN n'), Num Integer)
  (SymFromIntegral (WordN n') Integer) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (WordN n'), Num Integer)
  (SymFromIntegral (WordN n') Integer) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Con (WordN n') (IntN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (WordN n'), Num (IntN n))
   (SymFromIntegral (WordN n') (IntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (IntN n))
  (SymFromIntegral (WordN n') (IntN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (IntN n))
  (SymFromIntegral (WordN n') (IntN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Con (WordN n') (WordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (WordN n'), Num (WordN n))
   (SymFromIntegral (WordN n') (WordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (WordN n))
  (SymFromIntegral (WordN n') (WordN n)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (WordN n))
  (SymFromIntegral (WordN n') (WordN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'Con (WordN n') (FP eb sb)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Con)
   (Integral (WordN n'), Num (FP eb sb))
   (SymFromIntegral (WordN n') (FP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (FP eb sb))
  (SymFromIntegral (WordN n') (FP eb sb)) =>
r
r = r
If
  (IsConMode 'Con)
  (Integral (WordN n'), Num (FP eb sb))
  (SymFromIntegral (WordN n') (FP eb sb)) =>
r
r

instance UnifiedFromIntegral 'Sym SymInteger SymAlgReal where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral SymInteger, Num SymAlgReal)
   (SymFromIntegral SymInteger SymAlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral SymInteger, Num SymAlgReal)
  (SymFromIntegral SymInteger SymAlgReal) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral SymInteger, Num SymAlgReal)
  (SymFromIntegral SymInteger SymAlgReal) =>
r
r

instance UnifiedFromIntegral 'Sym SymInteger SymInteger where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral SymInteger, Num SymInteger)
   (SymFromIntegral SymInteger SymInteger) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral SymInteger, Num SymInteger)
  (SymFromIntegral SymInteger SymInteger) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral SymInteger, Num SymInteger)
  (SymFromIntegral SymInteger SymInteger) =>
r
r

instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymIntN n) where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral SymInteger, Num (SymIntN n))
   (SymFromIntegral SymInteger (SymIntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymIntN n))
  (SymFromIntegral SymInteger (SymIntN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymIntN n))
  (SymFromIntegral SymInteger (SymIntN n)) =>
r
r

instance
  (KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Sym SymInteger (SymWordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral SymInteger, Num (SymWordN n))
   (SymFromIntegral SymInteger (SymWordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymWordN n))
  (SymFromIntegral SymInteger (SymWordN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymWordN n))
  (SymFromIntegral SymInteger (SymWordN n)) =>
r
r

instance (ValidFP eb sb) => UnifiedFromIntegral 'Sym SymInteger (SymFP eb sb) where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral SymInteger, Num (SymFP eb sb))
   (SymFromIntegral SymInteger (SymFP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymFP eb sb))
  (SymFromIntegral SymInteger (SymFP eb sb)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral SymInteger, Num (SymFP eb sb))
  (SymFromIntegral SymInteger (SymFP eb sb)) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Sym (SymIntN n') SymAlgReal
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymIntN n'), Num SymAlgReal)
   (SymFromIntegral (SymIntN n') SymAlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num SymAlgReal)
  (SymFromIntegral (SymIntN n') SymAlgReal) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num SymAlgReal)
  (SymFromIntegral (SymIntN n') SymAlgReal) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Sym (SymIntN n') SymInteger
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymIntN n'), Num SymInteger)
   (SymFromIntegral (SymIntN n') SymInteger) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num SymInteger)
  (SymFromIntegral (SymIntN n') SymInteger) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num SymInteger)
  (SymFromIntegral (SymIntN n') SymInteger) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Sym (SymIntN n') (SymIntN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymIntN n'), Num (SymIntN n))
   (SymFromIntegral (SymIntN n') (SymIntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymIntN n))
  (SymFromIntegral (SymIntN n') (SymIntN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymIntN n))
  (SymFromIntegral (SymIntN n') (SymIntN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Sym (SymIntN n') (SymWordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymIntN n'), Num (SymWordN n))
   (SymFromIntegral (SymIntN n') (SymWordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymWordN n))
  (SymFromIntegral (SymIntN n') (SymWordN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymWordN n))
  (SymFromIntegral (SymIntN n') (SymWordN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'Sym (SymIntN n') (SymFP eb sb)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymIntN n'), Num (SymFP eb sb))
   (SymFromIntegral (SymIntN n') (SymFP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymFP eb sb))
  (SymFromIntegral (SymIntN n') (SymFP eb sb)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymIntN n'), Num (SymFP eb sb))
  (SymFromIntegral (SymIntN n') (SymFP eb sb)) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Sym (SymWordN n') SymAlgReal
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymWordN n'), Num SymAlgReal)
   (SymFromIntegral (SymWordN n') SymAlgReal) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num SymAlgReal)
  (SymFromIntegral (SymWordN n') SymAlgReal) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num SymAlgReal)
  (SymFromIntegral (SymWordN n') SymAlgReal) =>
r
r

instance
  (KnownNat n', 1 <= n') =>
  UnifiedFromIntegral 'Sym (SymWordN n') SymInteger
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymWordN n'), Num SymInteger)
   (SymFromIntegral (SymWordN n') SymInteger) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num SymInteger)
  (SymFromIntegral (SymWordN n') SymInteger) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num SymInteger)
  (SymFromIntegral (SymWordN n') SymInteger) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Sym (SymWordN n') (SymIntN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymWordN n'), Num (SymIntN n))
   (SymFromIntegral (SymWordN n') (SymIntN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymIntN n))
  (SymFromIntegral (SymWordN n') (SymIntN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymIntN n))
  (SymFromIntegral (SymWordN n') (SymIntN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>
  UnifiedFromIntegral 'Sym (SymWordN n') (SymWordN n)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymWordN n'), Num (SymWordN n))
   (SymFromIntegral (SymWordN n') (SymWordN n)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymWordN n))
  (SymFromIntegral (SymWordN n') (SymWordN n)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymWordN n))
  (SymFromIntegral (SymWordN n') (SymWordN n)) =>
r
r

instance
  (KnownNat n', 1 <= n', ValidFP eb sb) =>
  UnifiedFromIntegral 'Sym (SymWordN n') (SymFP eb sb)
  where
  withBaseFromIntegral :: forall r.
(If
   (IsConMode 'Sym)
   (Integral (SymWordN n'), Num (SymFP eb sb))
   (SymFromIntegral (SymWordN n') (SymFP eb sb)) =>
 r)
-> r
withBaseFromIntegral If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymFP eb sb))
  (SymFromIntegral (SymWordN n') (SymFP eb sb)) =>
r
r = r
If
  (IsConMode 'Sym)
  (Integral (SymWordN n'), Num (SymFP eb sb))
  (SymFromIntegral (SymWordN n') (SymFP eb sb)) =>
r
r