{-# LANGUAGE CPP
           , KindSignatures
           , DataKinds
           , GADTs
           , StandaloneDeriving
           , ExistentialQuantification
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2015.12.18
-- |
-- Module      :  Language.Hakaru.Types.Coercion
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Our theory of coercions for Hakaru's numeric hierarchy.
----------------------------------------------------------------
module Language.Hakaru.Types.Coercion
    (
    -- * The primitive coercions
      PrimCoercion(..)
    , PrimCoerce(..)

    -- * The category of general coercions
    , Coercion(..)
    , singletonCoercion
    , signed
    , continuous
    , Coerce(..)
    , singCoerceDom
    , singCoerceCod
    , singCoerceDomCod

    -- * The induced coercion hierarchy
    , CoercionMode(..)
    , findCoercion
    , findEitherCoercion
    , Lub(..)
    , findLub
    , SomeRing(..)
    , findRing
    , SomeFractional(..)
    , findFractional

    -- * Experimental optimization functions
    {-
    , CoerceTo_UnsafeFrom(..)
    , simplifyCTUF
    , UnsafeFrom_CoerceTo(..)
    , simplifyUFCT
    -}
    , ZigZag(..)
    , simplifyZZ
    ) where

import Prelude          hiding (id, (.))
import Control.Category (Category(..))
#if __GLASGOW_HASKELL__ < 710
import Data.Functor        ((<$>))
#endif
import Control.Applicative ((<|>))
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.IClasses
    (TypeEq(..), Eq1(..), Eq2(..), JmEq1(..), JmEq2(..))

----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: (?) coercing HMeasure by coercing the underlying measure space.
-- TODO: lifting coercion over (:->), to avoid the need for eta-expansion
-- TODO: lifting coersion over datatypes, to avoid traversing them at runtime
-- TODO: see how GHC handles lifting coersions these days...

-- N.B., we don't need to store the dictionary values here, we can recover them by typeclass (using -XScopedTypeVariables).
--
-- | Primitive proofs of the inclusions in our numeric hierarchy.
data PrimCoercion :: Hakaru -> Hakaru -> * where
    Signed     :: !(HRing a)       -> PrimCoercion (NonNegative a) a
    Continuous :: !(HContinuous a) -> PrimCoercion (HIntegral   a) a

-- TODO: instance Read (PrimCoercion a b)
deriving instance Show (PrimCoercion a b)

instance Eq (PrimCoercion a b) where -- this one could be derived
    == :: PrimCoercion a b -> PrimCoercion a b -> Bool
(==) = PrimCoercion a b -> PrimCoercion a b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (PrimCoercion a) where
    eq1 :: PrimCoercion a i -> PrimCoercion a i -> Bool
eq1 = PrimCoercion a i -> PrimCoercion a i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq2 PrimCoercion where
    eq2 :: PrimCoercion i j -> PrimCoercion i j -> Bool
eq2 PrimCoercion i j
x PrimCoercion i j
y = Bool
-> ((TypeEq i i, TypeEq j j) -> Bool)
-> Maybe (TypeEq i i, TypeEq j j)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> (TypeEq i i, TypeEq j j) -> Bool
forall a b. a -> b -> a
const Bool
True) (PrimCoercion i j
-> PrimCoercion i j -> Maybe (TypeEq i i, TypeEq j j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion i j
x PrimCoercion i j
y)
instance JmEq1 (PrimCoercion a) where
    jmEq1 :: PrimCoercion a i -> PrimCoercion a j -> Maybe (TypeEq i j)
jmEq1 PrimCoercion a i
x PrimCoercion a j
y = (TypeEq a a, TypeEq i j) -> TypeEq i j
forall a b. (a, b) -> b
snd ((TypeEq a a, TypeEq i j) -> TypeEq i j)
-> Maybe (TypeEq a a, TypeEq i j) -> Maybe (TypeEq i j)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimCoercion a i
-> PrimCoercion a j -> Maybe (TypeEq a a, TypeEq i j)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion a i
x PrimCoercion a j
y
instance JmEq2 PrimCoercion where
    jmEq2 :: PrimCoercion i1 j1
-> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 (Signed HRing j1
r1) (Signed HRing j2
r2) =
        HRing j1 -> HRing j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HRing j1
r1 HRing j2
r2 Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 (Continuous HContinuous j1
c1) (Continuous HContinuous j2
c2) =
        HContinuous j1 -> HContinuous j2 -> Maybe (TypeEq j1 j2)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 HContinuous j1
c1 HContinuous j2
c2 Maybe (TypeEq j1 j2)
-> (TypeEq j1 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2))
-> Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq j1 j2
Refl -> (TypeEq i1 i1, TypeEq j1 j1) -> Maybe (TypeEq i1 i1, TypeEq j1 j1)
forall a. a -> Maybe a
Just (TypeEq i1 i1
forall k (a :: k). TypeEq a a
Refl, TypeEq j1 j1
forall k (a :: k). TypeEq a a
Refl)
    jmEq2 PrimCoercion i1 j1
_ PrimCoercion i2 j2
_ = Maybe (TypeEq i1 i2, TypeEq j1 j2)
forall a. Maybe a
Nothing


----------------------------------------------------------------
-- | General proofs of the inclusions in our numeric hierarchy.
-- Notably, being a partial order, 'Coercion' forms a category. In
-- addition to the 'Category' instance, we also have the class
-- 'Coerce' for functors from 'Coercion' to the category of Haskell
-- functions, and you can get the co\/domain objects (via
-- 'singCoerceDom', 'singCoerceCod', or 'singCoerceDomCod').
data Coercion :: Hakaru -> Hakaru -> * where
    -- BUG: haddock doesn't like annotations on GADT constructors
    -- <https://github.com/hakaru-dev/hakaru/issues/6>

    -- Added the trivial coercion so we get the Category instance.
    -- This may/should make program transformations easier to write
    -- by allowing more intermediate ASTs, but will require a cleanup
    -- pass afterwards to remove the trivial coercions.
    CNil :: Coercion a a

    -- TODO: but sometimes we need the snoc-based inductive hypothesis...
    -- We use a cons-based approach rather than append-based in
    -- order to get a better inductive hypothesis.
    CCons :: !(PrimCoercion a b) -> !(Coercion b c) -> Coercion a c

infixr 5 `CCons`

-- TODO: instance Read (Coercion a b)
deriving instance Show (Coercion a b)

instance Eq  (Coercion a b) where
    == :: Coercion a b -> Coercion a b -> Bool
(==) = Coercion a b -> Coercion a b -> Bool
forall k (a :: k -> *) (i :: k). Eq1 a => a i -> a i -> Bool
eq1
instance Eq1 (Coercion a) where
    eq1 :: Coercion a i -> Coercion a i -> Bool
eq1 = Coercion a i -> Coercion a i -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2
instance Eq2 Coercion where
    eq2 :: Coercion i j -> Coercion i j -> Bool
eq2 Coercion i j
CNil         Coercion i j
CNil         = Bool
True
    eq2 (CCons PrimCoercion i b
x Coercion b j
xs) (CCons PrimCoercion i b
y Coercion b j
ys) =
      case PrimCoercion i b
-> PrimCoercion i b -> Maybe (TypeEq i i, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion i b
x PrimCoercion i b
y of
         Just (TypeEq i i
Refl, TypeEq b b
Refl) -> Coercion b j -> Coercion b j -> Bool
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Eq2 a =>
a i j -> a i j -> Bool
eq2 Coercion b j
xs Coercion b j
Coercion b j
ys
         Maybe (TypeEq i i, TypeEq b b)
Nothing -> Bool
False
    eq2 Coercion i j
_            Coercion i j
_            = Bool
False

-- TODO: the JmEq2 and JmEq1 instances

instance Category Coercion where
    id :: Coercion a a
id = Coercion a a
forall (a :: Hakaru). Coercion a a
CNil
    Coercion b c
xs . :: Coercion b c -> Coercion a b -> Coercion a c
. Coercion a b
CNil       = Coercion b c
Coercion a c
xs
    Coercion b c
xs . CCons PrimCoercion a b
y Coercion b b
ys = PrimCoercion a b -> Coercion b c -> Coercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
y (Coercion b c
xs Coercion b c -> Coercion b b -> Coercion b c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b
ys)


-- BUG: GHC 7.8 does not allow making these into pattern synonyms:
-- (1) it disallows standalone type signatures for pattern synonyms,
-- so we'd need to give it as an annotation, which isn't too terrible;
-- but, (2) it does not allow polymorphic pattern synonyms :(

-- | A smart constructor for lifting 'PrimCoercion' into 'Coercion'
singletonCoercion :: PrimCoercion a b -> Coercion a b
singletonCoercion :: PrimCoercion a b -> Coercion a b
singletonCoercion PrimCoercion a b
c = PrimCoercion a b -> Coercion b b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
c Coercion b b
forall (a :: Hakaru). Coercion a a
CNil

-- | A smart constructor for 'Signed'.
signed :: (HRing_ a) => Coercion (NonNegative a) a
signed :: Coercion (NonNegative a) a
signed = PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a
forall (a :: Hakaru) (b :: Hakaru).
PrimCoercion a b -> Coercion a b
singletonCoercion (PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a)
-> PrimCoercion (NonNegative a) a -> Coercion (NonNegative a) a
forall a b. (a -> b) -> a -> b
$ HRing a -> PrimCoercion (NonNegative a) a
forall (a :: Hakaru). HRing a -> PrimCoercion (NonNegative a) a
Signed HRing a
forall (a :: Hakaru). HRing_ a => HRing a
hRing

-- | A smart constructor for 'Continuous'.
continuous :: (HContinuous_ a) => Coercion (HIntegral a) a
continuous :: Coercion (HIntegral a) a
continuous = PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a
forall (a :: Hakaru) (b :: Hakaru).
PrimCoercion a b -> Coercion a b
singletonCoercion (PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a)
-> PrimCoercion (HIntegral a) a -> Coercion (HIntegral a) a
forall a b. (a -> b) -> a -> b
$ HContinuous a -> PrimCoercion (HIntegral a) a
forall (a :: Hakaru). HContinuous a -> PrimCoercion (HIntegral a) a
Continuous HContinuous a
forall (a :: Hakaru). HContinuous_ a => HContinuous a
hContinuous


----------------------------------------------------------------
-- | This class defines a mapping from 'PrimCoercion' to the @(->)@
-- category. (Technically these mappings aren't functors, since
-- 'PrimCoercion' doesn't form a category.) It's mostly used for
-- defining the analogous 'Coerce' instance; that is, given a
-- @PrimCoerce F@ instance, we have the following canonical @Coerce
-- F@ instance:
--
-- > instance Coerce F where
-- >     coerceTo   CNil         s = s
-- >     coerceTo   (CCons c cs) s = coerceTo cs (primCoerceTo c s)
-- >
-- >     coerceFrom CNil         s = s
-- >     coerceFrom (CCons c cs) s = primCoerceFrom c (coerceFrom cs s)
--
class PrimCoerce (f :: Hakaru -> *) where
    primCoerceTo   :: PrimCoercion a b -> f a -> f b
    primCoerceFrom :: PrimCoercion a b -> f b -> f a

instance PrimCoerce (Sing :: Hakaru -> *) where
    primCoerceTo :: PrimCoercion a b -> Sing a -> Sing b
primCoerceTo (Signed HRing b
theRing) Sing a
s =
        case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s (HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing) of
        Just TypeEq a a
Refl -> HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing b
theRing
        Maybe (TypeEq a a)
Nothing   -> String -> Sing b
forall a. HasCallStack => String -> a
error String
"primCoerceTo@Sing: the impossible happened"
    primCoerceTo (Continuous HContinuous b
theCont) Sing a
s =
        case Sing a -> Sing a -> Maybe (TypeEq a a)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
s (HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral HContinuous b
theCont) of
        Just TypeEq a a
Refl -> HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont
        Maybe (TypeEq a a)
Nothing   -> String -> Sing b
forall a. HasCallStack => String -> a
error String
"primCoerceTo@Sing: the impossible happened"

    primCoerceFrom :: PrimCoercion a b -> Sing b -> Sing a
primCoerceFrom (Signed HRing b
theRing) Sing b
s =
        case Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
s (HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing HRing b
theRing) of
        Just TypeEq b b
Refl -> HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing
        Maybe (TypeEq b b)
Nothing   -> String -> Sing a
forall a. HasCallStack => String -> a
error String
"primCoerceFrom@Sing: the impossible happened"
    primCoerceFrom (Continuous HContinuous b
theCont) Sing b
s =
        case Sing b -> Sing b -> Maybe (TypeEq b b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing b
s (HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont) of
        Just TypeEq b b
Refl -> HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral HContinuous b
theCont
        Maybe (TypeEq b b)
Nothing   -> String -> Sing a
forall a. HasCallStack => String -> a
error String
"primCoerceFrom@Sing: the impossible happened"


-- | This class defines functors from the 'Coercion' category to
-- the @(->)@ category. It's mostly used for defining smart
-- constructors that implement the coercion in @f@. We don't require
-- a 'PrimCoerce' constraint (because we never need it), but given
-- a @Coerce F@ instance, we have the following canonical @PrimCoerce
-- F@ instance:
--
-- > instance PrimCoerce F where
-- >     primCoerceTo   c = coerceTo   (singletonCoercion c)
-- >     primCoerceFrom c = coerceFrom (singletonCoercion c)
--
class Coerce (f :: Hakaru -> *) where
    coerceTo   :: Coercion a b -> f a -> f b
    coerceFrom :: Coercion a b -> f b -> f a

instance Coerce (Sing :: Hakaru -> *) where
    coerceTo :: Coercion a b -> Sing a -> Sing b
coerceTo   Coercion a b
CNil         Sing a
s = Sing a
Sing b
s
    coerceTo   (CCons PrimCoercion a b
c Coercion b b
cs) Sing a
s = Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (PrimCoercion a b -> Sing a -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f a -> f b
primCoerceTo PrimCoercion a b
c Sing a
s)

    coerceFrom :: Coercion a b -> Sing b -> Sing a
coerceFrom Coercion a b
CNil         Sing b
s = Sing a
Sing b
s
    coerceFrom (CCons PrimCoercion a b
c Coercion b b
cs) Sing b
s = PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f b -> f a
coerceFrom Coercion b b
cs Sing b
s)

----------------------------------------------------------------
singPrimCoerceDom :: PrimCoercion a b -> Sing a
singPrimCoerceDom :: PrimCoercion a b -> Sing a
singPrimCoerceDom (Signed     HRing b
theRing) = HRing b -> Sing (NonNegative b)
forall (a :: Hakaru). HRing a -> Sing (NonNegative a)
sing_NonNegative HRing b
theRing
singPrimCoerceDom (Continuous HContinuous b
theCont) = HContinuous b -> Sing (HIntegral b)
forall (a :: Hakaru). HContinuous a -> Sing (HIntegral a)
sing_HIntegral   HContinuous b
theCont

singPrimCoerceCod :: PrimCoercion a b -> Sing b
singPrimCoerceCod :: PrimCoercion a b -> Sing b
singPrimCoerceCod (Signed     HRing b
theRing) = HRing b -> Sing b
forall (a :: Hakaru). HRing a -> Sing a
sing_HRing       HRing b
theRing
singPrimCoerceCod (Continuous HContinuous b
theCont) = HContinuous b -> Sing b
forall (a :: Hakaru). HContinuous a -> Sing a
sing_HContinuous HContinuous b
theCont


-- | Return a singleton for the domain type, or 'Nothing' if it's
-- the 'CNil' coercion.
singCoerceDom :: Coercion a b -> Maybe (Sing a)
singCoerceDom :: Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion a b
CNil           = Maybe (Sing a)
forall a. Maybe a
Nothing
singCoerceDom (CCons PrimCoercion a b
c Coercion b b
CNil) = Sing a -> Maybe (Sing a)
forall a. a -> Maybe a
Just (Sing a -> Maybe (Sing a)) -> Sing a -> Maybe (Sing a)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing a
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing a
singPrimCoerceDom PrimCoercion a b
c
singCoerceDom (CCons PrimCoercion a b
c Coercion b b
cs)   = PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c (Sing b -> Sing a) -> Maybe (Sing b) -> Maybe (Sing a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion b b -> Maybe (Sing b)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion b b
cs

-- | Return a singleton for the codomain type, or 'Nothing' if it's
-- the 'CNil' coercion.
singCoerceCod :: Coercion a b -> Maybe (Sing b)
singCoerceCod :: Coercion a b -> Maybe (Sing b)
singCoerceCod Coercion a b
CNil           = Maybe (Sing b)
forall a. Maybe a
Nothing
singCoerceCod (CCons PrimCoercion a b
c Coercion b b
CNil) = Sing b -> Maybe (Sing b)
forall a. a -> Maybe a
Just (Sing b -> Maybe (Sing b)) -> Sing b -> Maybe (Sing b)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c
singCoerceCod (CCons PrimCoercion a b
c Coercion b b
cs)   = Sing b -> Maybe (Sing b)
forall a. a -> Maybe a
Just (Sing b -> Maybe (Sing b))
-> (Sing b -> Sing b) -> Sing b -> Maybe (Sing b)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (Sing b -> Maybe (Sing b)) -> Sing b -> Maybe (Sing b)
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c

-- | Return singletons for the domain and codomain types, or 'Nothing'
-- if it's the 'CNil' coercion. If you need both types, this is a
-- bit more efficient than calling 'singCoerceDom' and 'singCoerceCod'
-- separately.
singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)
singCoerceDomCod :: Coercion a b -> Maybe (Sing a, Sing b)
singCoerceDomCod Coercion a b
CNil           = Maybe (Sing a, Sing b)
forall a. Maybe a
Nothing
singCoerceDomCod (CCons PrimCoercion a b
c Coercion b b
CNil) =
    (Sing a, Sing b) -> Maybe (Sing a, Sing b)
forall a. a -> Maybe a
Just (PrimCoercion a b -> Sing a
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing a
singPrimCoerceDom PrimCoercion a b
c, PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c)
singCoerceDomCod (CCons PrimCoercion a b
c Coercion b b
cs)   = do
    Sing b
dom <- Coercion b b -> Maybe (Sing b)
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Maybe (Sing a)
singCoerceDom Coercion b b
cs
    (Sing a, Sing b) -> Maybe (Sing a, Sing b)
forall a. a -> Maybe a
Just (PrimCoercion a b -> Sing b -> Sing a
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
PrimCoerce f =>
PrimCoercion a b -> f b -> f a
primCoerceFrom PrimCoercion a b
c Sing b
dom
        , Coercion b b -> Sing b -> Sing b
forall (f :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
Coerce f =>
Coercion a b -> f a -> f b
coerceTo Coercion b b
cs (Sing b -> Sing b) -> Sing b -> Sing b
forall a b. (a -> b) -> a -> b
$ PrimCoercion a b -> Sing b
forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b
singPrimCoerceCod PrimCoercion a b
c
        )


----------------------------------------------------------------
----------------------------------------------------------------

-- | Given two types, find a coercion from the first to the second,
-- or return 'Nothing' if there is no such coercion.
findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing a
SNat  Sing b
SInt  = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findCoercion Sing a
SProb Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findCoercion Sing a
SNat  Sing b
SProb = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findCoercion Sing a
SInt  Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findCoercion Sing a
SNat  Sing b
SReal = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just (Coercion 'HInt b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt b -> Coercion a 'HInt -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findCoercion Sing a
a     Sing b
b     = Sing a -> Sing b -> Maybe (TypeEq a b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing b
b Maybe (TypeEq a b)
-> (TypeEq a b -> Maybe (Coercion a b)) -> Maybe (Coercion a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a b
Refl -> Coercion a a -> Maybe (Coercion a a)
forall a. a -> Maybe a
Just Coercion a a
forall (a :: Hakaru). Coercion a a
CNil


-- | Given two types, find a coercion where an unsafe
-- coercion, followed by a safe coercion are needed to
-- coerce the first type into the second, return otherwise
findMixedCoercion
    :: Sing a
    -> Sing b
    -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion :: Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion Sing a
SProb Sing b
SInt  = (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. a -> Maybe a
Just (Sing 'HNat
SNat, Coercion 'HNat a
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous, Coercion 'HNat b
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findMixedCoercion Sing a
SInt  Sing b
SProb = (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. a -> Maybe a
Just (Sing 'HNat
SNat, Coercion 'HNat a
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed, Coercion 'HNat b
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findMixedCoercion Sing a
_     Sing b
_     = Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall a. Maybe a
Nothing

data CoercionMode a b = 
              Safe   (Coercion a b)
  |           Unsafe (Coercion b a)
  | forall c. Mixed  (Sing c, Coercion c a, Coercion c b)                

-- | Given two types, find either a coercion from the first to the
-- second or a coercion from the second to the first, or returns
-- 'Nothing' if there is neither such coercion.
--
-- If the two types are equal, then we preferentially return the
-- @Coercion a b@. The ordering of the 'Either' is so that we
-- consider the @Coercion a b@ direction \"success\" in the 'Either'
-- monad (which also expresses our bias when the types are equal).
findEitherCoercion
    :: Sing a
    -> Sing b
    -> Maybe (CoercionMode a b)
findEitherCoercion :: Sing a -> Sing b -> Maybe (CoercionMode a b)
findEitherCoercion Sing a
a Sing b
b =
    (Coercion a b -> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru).
Coercion a b -> CoercionMode a b
Safe   (Coercion a b -> CoercionMode a b)
-> Maybe (Coercion a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a -> Sing b -> Maybe (Coercion a b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing a
a Sing b
b) Maybe (CoercionMode a b)
-> Maybe (CoercionMode a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    (Coercion b a -> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru).
Coercion b a -> CoercionMode a b
Unsafe (Coercion b a -> CoercionMode a b)
-> Maybe (Coercion b a) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing b -> Sing a -> Maybe (Coercion b a)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Maybe (Coercion a b)
findCoercion Sing b
b Sing a
a) Maybe (CoercionMode a b)
-> Maybe (CoercionMode a b) -> Maybe (CoercionMode a b)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
    ((Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> CoercionMode a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
(Sing c, Coercion c a, Coercion c b) -> CoercionMode a b
Mixed  ((Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
 -> CoercionMode a b)
-> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
-> Maybe (CoercionMode a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
forall (a :: Hakaru) (b :: Hakaru).
Sing a
-> Sing b -> Maybe (Sing 'HNat, Coercion 'HNat a, Coercion 'HNat b)
findMixedCoercion Sing a
a Sing b
b)


-- | An upper bound of two types, with the coercions witnessing its
-- upperbound-ness. The type itself ensures that we have /some/
-- upper bound; but in practice we assume it is in fact the /least/
-- upper bound.
data Lub (a :: Hakaru) (b :: Hakaru)
    = forall c. Lub !(Sing c) !(Coercion a c) !(Coercion b c)


-- TODO: is there any way we can reuse 'findCoercion' to DRY?
-- | Given two types, find their least upper bound.
findLub :: Sing a -> Sing b -> Maybe (Lub a b)
-- cases where @a < b@:
findLub :: Sing a -> Sing b -> Maybe (Lub a b)
findLub Sing a
SNat  Sing b
SInt  = Lub a 'HInt -> Maybe (Lub a 'HInt)
forall a. a -> Maybe a
Just (Lub a 'HInt -> Maybe (Lub a 'HInt))
-> Lub a 'HInt -> Maybe (Lub a 'HInt)
forall a b. (a -> b) -> a -> b
$ Sing 'HInt
-> Coercion a 'HInt -> Coercion 'HInt 'HInt -> Lub a 'HInt
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HInt
SInt  Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SProb Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SNat  Sing b
SProb = Lub a 'HProb -> Maybe (Lub a 'HProb)
forall a. a -> Maybe a
Just (Lub a 'HProb -> Maybe (Lub a 'HProb))
-> Lub a 'HProb -> Maybe (Lub a 'HProb)
forall a b. (a -> b) -> a -> b
$ Sing 'HProb
-> Coercion a 'HProb -> Coercion 'HProb 'HProb -> Lub a 'HProb
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HProb
SProb Coercion a 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SInt  Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
findLub Sing a
SNat  Sing b
SReal = Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a. a -> Maybe a
Just (Lub a 'HReal -> Maybe (Lub a 'HReal))
-> Lub a 'HReal -> Maybe (Lub a 'HReal)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion a 'HReal -> Coercion 'HReal 'HReal -> Lub a 'HReal
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal (Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt 'HReal -> Coercion a 'HInt -> Coercion a 'HReal
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed) Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil
-- the symmetric cases where @b < a@:
findLub Sing a
SInt  Sing b
SNat  = Lub 'HInt b -> Maybe (Lub 'HInt b)
forall a. a -> Maybe a
Just (Lub 'HInt b -> Maybe (Lub 'HInt b))
-> Lub 'HInt b -> Maybe (Lub 'HInt b)
forall a b. (a -> b) -> a -> b
$ Sing 'HInt
-> Coercion 'HInt 'HInt -> Coercion b 'HInt -> Lub 'HInt b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HInt
SInt  Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SReal Sing b
SProb = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SProb Sing b
SNat  = Lub 'HProb b -> Maybe (Lub 'HProb b)
forall a. a -> Maybe a
Just (Lub 'HProb b -> Maybe (Lub 'HProb b))
-> Lub 'HProb b -> Maybe (Lub 'HProb b)
forall a b. (a -> b) -> a -> b
$ Sing 'HProb
-> Coercion 'HProb 'HProb -> Coercion b 'HProb -> Lub 'HProb b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HProb
SProb Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findLub Sing a
SReal Sing b
SInt  = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil Coercion b 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
findLub Sing a
SReal Sing b
SNat  = Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a. a -> Maybe a
Just (Lub 'HReal b -> Maybe (Lub 'HReal b))
-> Lub 'HReal b -> Maybe (Lub 'HReal b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal
-> Coercion 'HReal 'HReal -> Coercion b 'HReal -> Lub 'HReal b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil (Coercion 'HInt 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion 'HInt 'HReal -> Coercion b 'HInt -> Coercion b 'HReal
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
-- cases where the lub is different from both @a@ and @b@:
findLub Sing a
SInt  Sing b
SProb = Lub a b -> Maybe (Lub a b)
forall a. a -> Maybe a
Just (Lub a b -> Maybe (Lub a b)) -> Lub a b -> Maybe (Lub a b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal -> Coercion a 'HReal -> Coercion b 'HReal -> Lub a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous Coercion b 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed
findLub Sing a
SProb Sing b
SInt  = Lub a b -> Maybe (Lub a b)
forall a. a -> Maybe a
Just (Lub a b -> Maybe (Lub a b)) -> Lub a b -> Maybe (Lub a b)
forall a b. (a -> b) -> a -> b
$ Sing 'HReal -> Coercion a 'HReal -> Coercion b 'HReal -> Lub a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing 'HReal
SReal Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed Coercion b 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous
-- case where @a == b@:
findLub Sing a
a     Sing b
b     = Sing a -> Sing b -> Maybe (TypeEq a b)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing a
a Sing b
b Maybe (TypeEq a b)
-> (TypeEq a b -> Maybe (Lub a b)) -> Maybe (Lub a b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TypeEq a b
Refl -> Lub a a -> Maybe (Lub a a)
forall a. a -> Maybe a
Just (Lub a a -> Maybe (Lub a a)) -> Lub a a -> Maybe (Lub a a)
forall a b. (a -> b) -> a -> b
$ Sing a -> Coercion a a -> Coercion a a -> Lub a a
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Sing c -> Coercion a c -> Coercion b c -> Lub a b
Lub Sing a
a Coercion a a
forall (a :: Hakaru). Coercion a a
CNil Coercion a a
forall (a :: Hakaru). Coercion a a
CNil


data SomeRing (a :: Hakaru)
    = forall b. SomeRing !(HRing b) !(Coercion a b)

-- | Give a type, finds the smallest coercion to another
-- with a HRing instance
findRing :: Sing a -> Maybe (SomeRing a)
findRing :: Sing a -> Maybe (SomeRing a)
findRing Sing a
SNat  = SomeRing a -> Maybe (SomeRing a)
forall a. a -> Maybe a
Just (HRing 'HInt -> Coercion a 'HInt -> SomeRing a
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HInt
HRing_Int  Coercion a 'HInt
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findRing Sing a
SInt  = SomeRing 'HInt -> Maybe (SomeRing 'HInt)
forall a. a -> Maybe a
Just (HRing 'HInt -> Coercion 'HInt 'HInt -> SomeRing 'HInt
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HInt
HRing_Int  Coercion 'HInt 'HInt
forall (a :: Hakaru). Coercion a a
CNil)
findRing Sing a
SProb = SomeRing a -> Maybe (SomeRing a)
forall a. a -> Maybe a
Just (HRing 'HReal -> Coercion a 'HReal -> SomeRing a
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HReal
HRing_Real Coercion a 'HReal
forall (a :: Hakaru). HRing_ a => Coercion (NonNegative a) a
signed)
findRing Sing a
SReal = SomeRing 'HReal -> Maybe (SomeRing 'HReal)
forall a. a -> Maybe a
Just (HRing 'HReal -> Coercion 'HReal 'HReal -> SomeRing 'HReal
forall (a :: Hakaru) (b :: Hakaru).
HRing b -> Coercion a b -> SomeRing a
SomeRing HRing 'HReal
HRing_Real Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil)
findRing Sing a
_     = Maybe (SomeRing a)
forall a. Maybe a
Nothing

data SomeFractional (a :: Hakaru)
    = forall b. SomeFractional !(HFractional b) !(Coercion a b)

-- | Give a type, finds the smallest coercion to another
-- with a HFractional instance
findFractional :: Sing a -> Maybe (SomeFractional a)
findFractional :: Sing a -> Maybe (SomeFractional a)
findFractional Sing a
SNat  = SomeFractional a -> Maybe (SomeFractional a)
forall a. a -> Maybe a
Just (HFractional 'HProb -> Coercion a 'HProb -> SomeFractional a
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HProb
HFractional_Prob Coercion a 'HProb
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findFractional Sing a
SInt  = SomeFractional a -> Maybe (SomeFractional a)
forall a. a -> Maybe a
Just (HFractional 'HReal -> Coercion a 'HReal -> SomeFractional a
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HReal
HFractional_Real Coercion a 'HReal
forall (a :: Hakaru). HContinuous_ a => Coercion (HIntegral a) a
continuous)
findFractional Sing a
SProb = SomeFractional 'HProb -> Maybe (SomeFractional 'HProb)
forall a. a -> Maybe a
Just (HFractional 'HProb
-> Coercion 'HProb 'HProb -> SomeFractional 'HProb
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HProb
HFractional_Prob Coercion 'HProb 'HProb
forall (a :: Hakaru). Coercion a a
CNil)
findFractional Sing a
SReal = SomeFractional 'HReal -> Maybe (SomeFractional 'HReal)
forall a. a -> Maybe a
Just (HFractional 'HReal
-> Coercion 'HReal 'HReal -> SomeFractional 'HReal
forall (a :: Hakaru) (b :: Hakaru).
HFractional b -> Coercion a b -> SomeFractional a
SomeFractional HFractional 'HReal
HFractional_Real Coercion 'HReal 'HReal
forall (a :: Hakaru). Coercion a a
CNil)
findFractional Sing a
_     = Maybe (SomeFractional a)
forall a. Maybe a
Nothing


----------------------------------------------------------------
----------------------------------------------------------------

data CoerceTo_UnsafeFrom :: Hakaru -> Hakaru -> * where
    CTUF :: !(Coercion b c) -> !(Coercion b a) -> CoerceTo_UnsafeFrom a c

-- BUG: deriving instance Eq   (CoerceTo_UnsafeFrom a b)
-- BUG: deriving instance Read (CoerceTo_UnsafeFrom a b)
deriving instance Show (CoerceTo_UnsafeFrom a b)

-- TODO: handle the fact that certain coercions commute over one another!
simplifyCTUF :: CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF :: CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (CTUF Coercion b c
xs Coercion b a
ys) =
    case Coercion b c
xs of
    Coercion b c
CNil        -> Coercion b b -> Coercion b a -> CoerceTo_UnsafeFrom a b
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b b
forall (a :: Hakaru). Coercion a a
CNil Coercion b a
ys
    CCons PrimCoercion b b
x Coercion b c
xs' ->
        case Coercion b a
ys of
        Coercion b a
CNil        -> Coercion b c -> Coercion b b -> CoerceTo_UnsafeFrom b c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs Coercion b b
forall (a :: Hakaru). Coercion a a
CNil
        CCons PrimCoercion b b
y Coercion b a
ys' ->
            case PrimCoercion b b
-> PrimCoercion b b -> Maybe (TypeEq b b, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion b b
x PrimCoercion b b
y of
            Just (TypeEq b b
Refl, TypeEq b b
Refl) -> CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
forall (a :: Hakaru) (c :: Hakaru).
CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs' Coercion b a
Coercion b a
ys')
            Maybe (TypeEq b b, TypeEq b b)
Nothing           -> Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b c
xs Coercion b a
ys

----------------------------------------------------------------
-- | Choose the other inductive hypothesis.
data RevCoercion :: Hakaru -> Hakaru -> * where
    CLin  :: RevCoercion a a
    CSnoc :: !(RevCoercion a b) -> !(PrimCoercion b c) -> RevCoercion a c

-- BUG: deriving instance Eq   (RevCoercion a b)
-- BUG: deriving instance Read (RevCoercion a b)
deriving instance Show (RevCoercion a b)

instance Category RevCoercion where
    id :: RevCoercion a a
id = RevCoercion a a
forall (a :: Hakaru). RevCoercion a a
CLin
    RevCoercion b c
CLin . :: RevCoercion b c -> RevCoercion a b -> RevCoercion a c
. RevCoercion a b
xs       = RevCoercion a b
RevCoercion a c
xs
    CSnoc RevCoercion b b
ys PrimCoercion b c
y . RevCoercion a b
xs = RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc (RevCoercion b b
ys RevCoercion b b -> RevCoercion a b -> RevCoercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. RevCoercion a b
xs) PrimCoercion b c
y

revCons :: PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons :: PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x RevCoercion b c
CLin         = RevCoercion a a -> PrimCoercion a b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc RevCoercion a a
forall (a :: Hakaru). RevCoercion a a
CLin PrimCoercion a b
x
revCons PrimCoercion a b
x (CSnoc RevCoercion b b
ys PrimCoercion b c
y) = RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
RevCoercion a b -> PrimCoercion b c -> RevCoercion a c
CSnoc (PrimCoercion a b -> RevCoercion b b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x RevCoercion b b
ys) PrimCoercion b c
y

toRev :: Coercion a b -> RevCoercion a b
toRev :: Coercion a b -> RevCoercion a b
toRev Coercion a b
CNil         = RevCoercion a b
forall (a :: Hakaru). RevCoercion a a
CLin
toRev (CCons PrimCoercion a b
x Coercion b b
xs) = PrimCoercion a b -> RevCoercion b b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> RevCoercion b c -> RevCoercion a c
revCons PrimCoercion a b
x (Coercion b b -> RevCoercion b b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion b b
xs)

obvSnoc :: Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc :: Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc Coercion a b
CNil         PrimCoercion b c
y = PrimCoercion b c -> Coercion c c -> Coercion b c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion b c
y Coercion c c
forall (a :: Hakaru). Coercion a a
CNil
obvSnoc (CCons PrimCoercion a b
x Coercion b b
xs) PrimCoercion b c
y = PrimCoercion a b -> Coercion b c -> Coercion a c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
PrimCoercion a b -> Coercion b c -> Coercion a c
CCons PrimCoercion a b
x (Coercion b b -> PrimCoercion b c -> Coercion b c
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc Coercion b b
xs PrimCoercion b c
y)

fromRev :: RevCoercion a b -> Coercion a b
fromRev :: RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
CLin         = Coercion a b
forall (a :: Hakaru). Coercion a a
CNil
fromRev (CSnoc RevCoercion a b
xs PrimCoercion b b
x) = Coercion a b -> PrimCoercion b b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> PrimCoercion b c -> Coercion a c
obvSnoc (RevCoercion a b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
xs) PrimCoercion b b
x

data UnsafeFrom_CoerceTo :: Hakaru -> Hakaru -> * where
    UFCT
        :: !(Coercion c b)
        -> !(Coercion a b)
        -> UnsafeFrom_CoerceTo a c

-- BUG: deriving instance Eq   (UnsafeFrom_CoerceTo a b)
-- BUG: deriving instance Read (UnsafeFrom_CoerceTo a b)
deriving instance Show (UnsafeFrom_CoerceTo a b)

data RevUFCT :: Hakaru -> Hakaru -> * where
    RevUFCT :: !(RevCoercion c b) -> !(RevCoercion a b) -> RevUFCT a c
        
-- TODO: handle the fact that certain coercions commute over one another!
-- N.B., This version can be tricky to get to type check because our associated type families aren't guaranteed injective.
simplifyUFCT :: UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT :: UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT (UFCT Coercion c b
xs Coercion a b
ys) =
    case RevUFCT a c -> RevUFCT a c
forall (a :: Hakaru) (c :: Hakaru). RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevUFCT a c -> RevUFCT a c) -> RevUFCT a c -> RevUFCT a c
forall a b. (a -> b) -> a -> b
$ RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT (Coercion c b -> RevCoercion c b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion c b
xs) (Coercion a b -> RevCoercion a b
forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> RevCoercion a b
toRev Coercion a b
ys) of
    RevUFCT RevCoercion c b
xs' RevCoercion a b
ys' -> Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
UFCT (RevCoercion c b -> Coercion c b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion c b
xs') (RevCoercion a b -> Coercion a b
forall (a :: Hakaru) (b :: Hakaru). RevCoercion a b -> Coercion a b
fromRev RevCoercion a b
ys')

simplifyRevUFCT :: RevUFCT a c -> RevUFCT a c
simplifyRevUFCT :: RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevUFCT RevCoercion c b
xs RevCoercion a b
ys) =
    case RevCoercion c b
xs of
    RevCoercion c b
CLin        -> RevCoercion b b -> RevCoercion a b -> RevUFCT a b
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion b b
forall (a :: Hakaru). RevCoercion a a
CLin RevCoercion a b
ys
    CSnoc RevCoercion c b
xs' PrimCoercion b b
x ->
        case RevCoercion a b
ys of
        RevCoercion a b
CLin        -> RevCoercion c b -> RevCoercion b b -> RevUFCT b c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs RevCoercion b b
forall (a :: Hakaru). RevCoercion a a
CLin
        CSnoc RevCoercion a b
ys' PrimCoercion b b
y ->
            case PrimCoercion b b
-> PrimCoercion b b -> Maybe (TypeEq b b, TypeEq b b)
forall k1 k2 (a :: k1 -> k2 -> *) (i1 :: k1) (j1 :: k2) (i2 :: k1)
       (j2 :: k2).
JmEq2 a =>
a i1 j1 -> a i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)
jmEq2 PrimCoercion b b
x PrimCoercion b b
y of
            Just (TypeEq b b
Refl, TypeEq b b
Refl) -> RevUFCT a c -> RevUFCT a c
forall (a :: Hakaru) (c :: Hakaru). RevUFCT a c -> RevUFCT a c
simplifyRevUFCT (RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs' RevCoercion a b
RevCoercion a b
ys')
            Maybe (TypeEq b b, TypeEq b b)
Nothing           -> RevCoercion c b -> RevCoercion a b -> RevUFCT a c
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
RevCoercion c b -> RevCoercion a b -> RevUFCT a c
RevUFCT RevCoercion c b
xs RevCoercion a b
ys


-- TODO: implement a simplifying pass for pushing/gathering coersions over other things (e.g., Less/Equal)

----------------------------------------------------------------
----------------------------------------------------------------

-- | An arbitrary composition of safe and unsafe coercions.
data ZigZag :: Hakaru -> Hakaru -> * where
    ZRefl :: ZigZag a a
    Zig   :: !(Coercion a b) -> !(ZigZag b c) -> ZigZag a c
    Zag   :: !(Coercion b a) -> !(ZigZag b c) -> ZigZag a c

-- BUG: deriving instance Eq   (ZigZag a b)
-- BUG: deriving instance Read (ZigZag a b)
deriving instance Show (ZigZag a b)

-- TODO: whenever we build up a new ZigZag from the remains of a simplification step, do we need to resimplify? If so, how can we avoid quadratic behavior? cf., <http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-normalization-rta.pdf> Also, try just doing a shortest-path problem on the graph of coercions (since we can get all the singletons along the way)
-- TODO: handle the fact that certain coercions commute over one another!
simplifyZZ :: ZigZag a b -> ZigZag a b
simplifyZZ :: ZigZag a b -> ZigZag a b
simplifyZZ ZigZag a b
ZRefl      = ZigZag a b
forall (a :: Hakaru). ZigZag a a
ZRefl
simplifyZZ (Zig Coercion a b
x ZigZag b b
xs) =
    case ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru). ZigZag a b -> ZigZag a b
simplifyZZ ZigZag b b
xs of
    ZigZag b b
ZRefl   -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x ZigZag b b
forall (a :: Hakaru). ZigZag a a
ZRefl
    Zig Coercion b b
y ZigZag b b
z -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig (Coercion b b
y Coercion b b -> Coercion a b -> Coercion a b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion a b
x) ZigZag b b
z
    Zag Coercion b b
y ZigZag b b
z ->
        -- TODO: can we optimize this to avoid reversing things?
        case UnsafeFrom_CoerceTo b a -> UnsafeFrom_CoerceTo b a
forall (a :: Hakaru) (c :: Hakaru).
UnsafeFrom_CoerceTo a c -> UnsafeFrom_CoerceTo a c
simplifyUFCT (Coercion a b -> Coercion b b -> UnsafeFrom_CoerceTo b a
forall (c :: Hakaru) (b :: Hakaru) (a :: Hakaru).
Coercion c b -> Coercion a b -> UnsafeFrom_CoerceTo a c
UFCT Coercion a b
x Coercion b b
y) of
        UFCT Coercion a b
CNil Coercion b b
CNil -> ZigZag a b
ZigZag b b
z
        UFCT Coercion a b
CNil Coercion b b
y'   -> Coercion b b -> ZigZag b b -> ZigZag b b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b b
y' ZigZag b b
z
        UFCT Coercion a b
x'   Coercion b b
CNil -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x' ZigZag b b
ZigZag b b
z
        UFCT Coercion a b
x'   Coercion b b
y'   -> Coercion a b -> ZigZag b b -> ZigZag a b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion a b
x' (Coercion b b -> ZigZag b b -> ZigZag b b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b b
y' ZigZag b b
z)
simplifyZZ (Zag Coercion b a
x ZigZag b b
xs) =
    case ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru). ZigZag a b -> ZigZag a b
simplifyZZ ZigZag b b
xs of
    ZigZag b b
ZRefl   -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x ZigZag b b
forall (a :: Hakaru). ZigZag a a
ZRefl
    Zag Coercion b b
y ZigZag b b
z -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag (Coercion b a
x Coercion b a -> Coercion b b -> Coercion b a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Coercion b b
y) ZigZag b b
z
    Zig Coercion b b
y ZigZag b b
z ->
        case CoerceTo_UnsafeFrom b a -> CoerceTo_UnsafeFrom b a
forall (a :: Hakaru) (c :: Hakaru).
CoerceTo_UnsafeFrom a c -> CoerceTo_UnsafeFrom a c
simplifyCTUF (Coercion b a -> Coercion b b -> CoerceTo_UnsafeFrom b a
forall (b :: Hakaru) (c :: Hakaru) (a :: Hakaru).
Coercion b c -> Coercion b a -> CoerceTo_UnsafeFrom a c
CTUF Coercion b a
x Coercion b b
y) of
        CTUF Coercion b a
CNil Coercion b b
CNil -> ZigZag a b
ZigZag b b
z
        CTUF Coercion b a
CNil Coercion b b
y'   -> Coercion b b -> ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion b b
y' ZigZag b b
z
        CTUF Coercion b a
x'   Coercion b b
CNil -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x' ZigZag b b
ZigZag b b
z
        CTUF Coercion b a
x'   Coercion b b
y'   -> Coercion b a -> ZigZag b b -> ZigZag a b
forall (b :: Hakaru) (a :: Hakaru) (c :: Hakaru).
Coercion b a -> ZigZag b c -> ZigZag a c
Zag Coercion b a
x' (Coercion b b -> ZigZag b b -> ZigZag b b
forall (a :: Hakaru) (b :: Hakaru) (c :: Hakaru).
Coercion a b -> ZigZag b c -> ZigZag a c
Zig Coercion b b
y' ZigZag b b
z)

----------------------------------------------------------------
----------------------------------------------------------- fin.