{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Support for reclassification
module Debug.RecoverRTTI.Reclassify (
    Reclassified(..)
  , reclassify_
  , distribReclassified
  , FromUsr(..)
  , coerceFromUsr
  ) where

import Data.Kind
import Data.SOP hiding (NS(..))
import Data.Void
import Unsafe.Coerce (unsafeCoerce)

import Debug.RecoverRTTI.Classifier
import Debug.RecoverRTTI.Tuple
import Debug.RecoverRTTI.Nat
import Debug.RecoverRTTI.Wrappers

-- | Reclassified values
--
-- Reclassification can be done by user code which want to take advantage of
-- the classification infrastructure for @recover-rtti@ but add some additional
-- classification for domain-specific types known only to that client code.
--
-- When we reclassify a value, a value that might previously be classified as
-- @UserDefined@ may now be classified as some concrete type; therefore we
-- compute a classifier for a potentially /different/ type along with
-- evidence that we can coerce between the two.
data Reclassified o a where
  Reclassified :: o b -> FromUsr a b -> Reclassified o a

-- | Extension of 'Reclassified' to multiple elems
--
-- This is used internally only.
data ReclassifiedElems o as where
  RElems ::
       (SListI bs, Length bs ~ Length as)
    => Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as

reclassify_ :: forall m o o'. Applicative m
  => (forall a. o a -> m (Reclassified o' a))
  -> (forall a. Classifier_ o a -> m (Classifier_ (Reclassified o') a))
reclassify_ :: (forall a. o a -> m (Reclassified o' a))
-> forall a. Classifier_ o a -> m (Classifier_ (Reclassified o') a)
reclassify_ = (forall a. o a -> m (Reclassified o' a))
-> Classifier_ o a -> m (Classifier_ (Reclassified o') a)
forall (m :: * -> *) (o :: * -> *) (o' :: * -> *).
Applicative m =>
(forall a. o a -> m (o' a))
-> forall a. Classifier_ o a -> m (Classifier_ o' a)
mapClassifier

-- | Lift 'Reclassified' to the top-level
--
-- Given a classifier with user-defined classifiers at the levels, along with
-- coercion functions, leave the user-defined classifiers in place but lift the
-- coercion function to the top-level.
distribReclassified :: forall o.
     (forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a)
distribReclassified :: Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
distribReclassified = Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
forall a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go
  where
    go :: forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
    -- Primitive and user-defined
    go :: Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go (C_Prim  PrimClassifier a
c) = Classifier_ o a -> FromUsr a a -> Reclassified (Classifier_ o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (PrimClassifier a -> Classifier_ o a
forall a (o :: * -> *). PrimClassifier a -> Classifier_ o a
C_Prim PrimClassifier a
c) FromUsr a a
forall a. FromUsr a a
Id
    go (C_Other Reclassified o a
c) = case Reclassified o a
c of Reclassified o b
c' FromUsr a b
f -> Classifier_ o b -> FromUsr a b -> Reclassified (Classifier_ o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (o b -> Classifier_ o b
forall (o :: * -> *) a. o a -> Classifier_ o a
C_Other o b
c') FromUsr a b
f

    -- Compound
    go (C_Maybe        Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Maybe a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Maybe a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Maybe a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Maybe a)
C_Maybe        Elems (Reclassified o) '[a]
c
    go (C_Either       Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (Either a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (Either a b)
forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall a' b'. Elems o '[a', b'] -> Classifier_ o (Either a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (Either a b)
C_Either       Elems (Reclassified o) '[a, b]
c
    go (C_List         Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o [a'])
-> Elems (Reclassified o) '[a] -> Reclassified (Classifier_ o) [a]
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o [a']
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o [a]
C_List         Elems (Reclassified o) '[a]
c
    go (C_Ratio        Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Ratio a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Ratio a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Ratio a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Ratio a)
C_Ratio        Elems (Reclassified o) '[a]
c
    go (C_Set          Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Set a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Set a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Set a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Set a)
C_Set          Elems (Reclassified o) '[a]
c
    go (C_Map          Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (Map a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (Map a b)
forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall a' b'. Elems o '[a', b'] -> Classifier_ o (Map a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (Map a b)
C_Map          Elems (Reclassified o) '[a, b]
c
    go (C_IntMap       Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (IntMap a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (IntMap a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (IntMap a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (IntMap a)
C_IntMap       Elems (Reclassified o) '[a]
c
    go (C_Sequence     Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Seq a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Seq a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Seq a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Seq a)
C_Sequence     Elems (Reclassified o) '[a]
c
    go (C_Tree         Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Tree a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Tree a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Tree a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Tree a)
C_Tree         Elems (Reclassified o) '[a]
c
    go (C_HashSet      Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (HashSet a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (HashSet a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (HashSet a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (HashSet a)
C_HashSet      Elems (Reclassified o) '[a]
c
    go (C_HashMap      Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (HashMap a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (HashMap a b)
forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall a' b'. Elems o '[a', b'] -> Classifier_ o (HashMap a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (HashMap a b)
C_HashMap      Elems (Reclassified o) '[a, b]
c
    go (C_HM_Array     Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Array a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Array a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Array a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Array a)
C_HM_Array     Elems (Reclassified o) '[a]
c
    go (C_Prim_Array   Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Array a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Array a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Array a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Array a)
C_Prim_Array   Elems (Reclassified o) '[a]
c
    go (C_Vector_Boxed Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Vector a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Vector a)
forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (Vector a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Vector a)
C_Vector_Boxed Elems (Reclassified o) '[a]
c
    go (C_Tuple        Elems (Reclassified o) xs
c) = (forall (as' :: [*]).
 (SListI as', Length as' ~ Length xs) =>
 Elems o as' -> Classifier_ o (WrappedTuple as'))
-> Elems (Reclassified o) xs
-> Reclassified (Classifier_ o) (WrappedTuple xs)
forall (f :: [*] -> *) (as :: [*]).
SListI as =>
(forall (as' :: [*]).
 (SListI as', Length as' ~ Length as) =>
 Elems o as' -> Classifier_ o (f as'))
-> Elems (Reclassified o) as -> Reclassified (Classifier_ o) (f as)
goN forall (as' :: [*]).
(SListI as', Length as' ~ Length xs) =>
Elems o as' -> Classifier_ o (WrappedTuple as')
forall (xs :: [*]) (o :: * -> *).
(SListI xs, IsValidSize (Length xs)) =>
Elems o xs -> Classifier_ o (WrappedTuple xs)
C_Tuple        Elems (Reclassified o) xs
c

    go1 :: forall f a.
         (forall a'. Elems o '[a'] -> Classifier_ o (f a'))
      -> Elems (Reclassified o) '[a]
      -> Reclassified (Classifier_ o) (f a)
    go1 :: (forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (f a')
cf Elems (Reclassified o) '[a]
c =
        case Elems (Reclassified o) '[a] -> ReclassifiedElems o '[a]
forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) '[a]
c of
          RElems Elems o bs
c' (PCons FromUsr x y
f PairWise FromUsr xs ys
PNil) -> Classifier_ o (f y)
-> FromUsr (f x) (f y) -> Reclassified (Classifier_ o) (f x)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o '[y] -> Classifier_ o (f y)
forall a'. Elems o '[a'] -> Classifier_ o (f a')
cf Elems o bs
Elems o '[y]
c') (FromUsr x y -> FromUsr (f x) (f y)
forall a1 b1 (f :: * -> *). FromUsr a1 b1 -> FromUsr (f a1) (f b1)
F1 FromUsr x y
f)

    go2 :: forall f a b.
         (forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
      -> Elems (Reclassified o) '[a, b]
      -> Reclassified (Classifier_ o) (f a b)
    go2 :: (forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b')
cf Elems (Reclassified o) '[a, b]
c =
        case Elems (Reclassified o) '[a, b] -> ReclassifiedElems o '[a, b]
forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) '[a, b]
c of
          RElems Elems o bs
c' (PCons FromUsr x y
f (PCons FromUsr x y
f' PairWise FromUsr xs ys
PNil)) -> Classifier_ o (f y y)
-> FromUsr (f x x) (f y y) -> Reclassified (Classifier_ o) (f x x)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o '[y, y] -> Classifier_ o (f y y)
forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b')
cf Elems o bs
Elems o '[y, y]
c') (FromUsr x y -> FromUsr x y -> FromUsr (f x x) (f y y)
forall a1 b1 a2 b2 (f :: * -> * -> *).
FromUsr a1 b1 -> FromUsr a2 b2 -> FromUsr (f a1 a2) (f b1 b2)
F2 FromUsr x y
f FromUsr x y
f')

    goN :: forall f as.
         SListI as
      => (forall as'.
               (SListI as', Length as' ~ Length as)
            => Elems o as' -> Classifier_ o (f as'))
      -> Elems (Reclassified o) as
      -> Reclassified (Classifier_ o) (f as)
    goN :: (forall (as' :: [*]).
 (SListI as', Length as' ~ Length as) =>
 Elems o as' -> Classifier_ o (f as'))
-> Elems (Reclassified o) as -> Reclassified (Classifier_ o) (f as)
goN forall (as' :: [*]).
(SListI as', Length as' ~ Length as) =>
Elems o as' -> Classifier_ o (f as')
cf Elems (Reclassified o) as
c =
        case Elems (Reclassified o) as -> ReclassifiedElems o as
forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) as
c of
          RElems Elems o bs
c' PairWise FromUsr as bs
fs -> Classifier_ o (f bs)
-> FromUsr (f as) (f bs) -> Reclassified (Classifier_ o) (f as)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o bs -> Classifier_ o (f bs)
forall (as' :: [*]).
(SListI as', Length as' ~ Length as) =>
Elems o as' -> Classifier_ o (f as')
cf Elems o bs
c') (PairWise FromUsr as bs -> FromUsr (f as) (f bs)
forall (as :: [*]) (bs :: [*]) (f :: [*] -> *).
PairWise FromUsr as bs -> FromUsr (f as) (f bs)
FN PairWise FromUsr as bs
fs)

distribElem :: Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem :: Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem = \case
    Elem (Reclassified o) a
NoElem -> Elem o Void -> FromUsr Void Void -> Reclassified (Elem o) Void
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified Elem o Void
forall (o :: * -> *). Elem o Void
NoElem FromUsr Void Void
forall a. FromUsr Void a
Absurd
    Elem Classifier_ (Reclassified o) a
c -> case Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
forall (o :: * -> *) a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
distribReclassified Classifier_ (Reclassified o) a
c of
                Reclassified Classifier_ o b
c' FromUsr a b
f -> Elem o b -> FromUsr a b -> Reclassified (Elem o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Classifier_ o b -> Elem o b
forall (o :: * -> *) a. Classifier_ o a -> Elem o a
Elem Classifier_ o b
c') FromUsr a b
f

distribElems ::
     SListI xs
  => Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems :: Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems = \(Elems NP (Elem (Reclassified o)) xs
cs) -> NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go (NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs)
-> NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
forall a b. (a -> b) -> a -> b
$ (forall a. Elem (Reclassified o) a -> Reclassified (Elem o) a)
-> NP (Elem (Reclassified o)) xs -> NP (Reclassified (Elem o)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall a. Elem (Reclassified o) a -> Reclassified (Elem o) a
forall (o :: * -> *) a.
Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem NP (Elem (Reclassified o)) xs
cs
  where
    go :: NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
    go :: NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go NP (Reclassified (Elem o)) xs
Nil                      = Elems o '[] -> PairWise FromUsr '[] '[] -> ReclassifiedElems o '[]
forall (bs :: [*]) (as :: [*]) (o :: * -> *).
(SListI bs, Length bs ~ Length as) =>
Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as
RElems (NP (Elem o) '[] -> Elems o '[]
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) '[]
forall k (a :: k -> *). NP a '[]
Nil) PairWise FromUsr '[] '[]
forall (f :: * -> * -> *). PairWise f '[] '[]
PNil
    go (Reclassified Elem o b
c FromUsr x b
f :* NP (Reclassified (Elem o)) xs
cs) = case NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go NP (Reclassified (Elem o)) xs
cs of
                                    RElems (Elems NP (Elem o) bs
cs') PairWise FromUsr xs bs
fs' ->
                                      Elems o (b : bs)
-> PairWise FromUsr (x : xs) (b : bs)
-> ReclassifiedElems o (x : xs)
forall (bs :: [*]) (as :: [*]) (o :: * -> *).
(SListI bs, Length bs ~ Length as) =>
Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as
RElems (NP (Elem o) (b : bs) -> Elems o (b : bs)
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems (Elem o b
c Elem o b -> NP (Elem o) bs -> NP (Elem o) (b : bs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (Elem o) bs
cs')) (FromUsr x b
-> PairWise FromUsr xs bs -> PairWise FromUsr (x : xs) (b : bs)
forall (f :: * -> * -> *) x y (xs :: [*]) (ys :: [*]).
f x y -> PairWise f xs ys -> PairWise f (x : xs) (y : ys)
PCons FromUsr x b
f PairWise FromUsr xs bs
fs')

{-------------------------------------------------------------------------------
  Evidence that we are only doing conversions from Any
-------------------------------------------------------------------------------}

-- | Evidence that we can convert between two types
--
-- The only actual conversion we ever do is from 'UserDefined' (aka 'Any') to
-- whatever type the reclassification gives.
data FromUsr :: Type -> Type -> Type where
  Id      :: FromUsr a a
  Absurd  :: FromUsr Void a
  FromUsr :: FromUsr UserDefined a
  F1      :: FromUsr a1 b1 -> FromUsr (f a1) (f b1)
  F2      :: FromUsr a1 b1 -> FromUsr a2 b2 -> FromUsr (f a1 a2) (f b1 b2)
  FN      :: PairWise FromUsr as bs -> FromUsr (f as) (f bs)
  Compose :: FromUsr b c -> FromUsr a b -> FromUsr a c

-- | Coerce, given some evidence that the coercion is sound.
coerceFromUsr :: FromUsr a b -> a -> b
coerceFromUsr :: FromUsr a b -> a -> b
coerceFromUsr = FromUsr a b -> a -> b
forall a b. a -> b
unsafeCoerce