-- |
-- Module      : Data.Manifold.WithBoundary
-- Copyright   : (c) Justus Sagemüller 2020
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE DefaultSignatures        #-}
{-# LANGUAGE DeriveGeneric            #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE UnicodeSyntax            #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE TypeInType               #-}
{-# LANGUAGE NoStarIsType             #-}
{-# LANGUAGE CPP                      #-}


module Data.Manifold.WithBoundary
        ( SemimanifoldWithBoundary(..), PseudoAffineWithBoundary(..), ProjectableBoundary(..)
        , SmfdWBoundWitness(..)
        , AdditiveMonoid(..), HalfSpace(..)
        ) where

import Data.Manifold.WithBoundary.Class

import Data.VectorSpace
import Data.AffineSpace
import Data.Basis

import Math.Manifold.Core.PseudoAffine
import Data.Manifold.PseudoAffine
import Math.Manifold.Core.Types
import Data.Manifold.Types.Primitive
import Math.Manifold.VectorSpace.ZeroDimensional
import Math.LinearMap.Category ( Tensor(..), TensorSpace(..)
                               , LinearMap(..), LinearFunction(..), LinearSpace(..)
                               , Num', closedScalarWitness, ClosedScalarWitness(..)
                               , DualSpaceWitness(..), ScalarSpaceWitness(..)
                               , LinearManifoldWitness(..) )
#if MIN_VERSION_linearmap_category(0,6,0)
import Math.VectorSpace.DimensionAware
                ( DimensionAware(..), Dimensional(..), DimensionalityWitness(..)
                , dimensionality, DimensionalityCases(..)
                , dimensionalitySing )
import GHC.TypeLits
#if MIN_VERSION_singletons(3,0,0)
import Prelude.Singletons (SNum(..))
import GHC.TypeLits.Singletons (withKnownNat, SNat(..))
#else
import Data.Singletons.Prelude.Num (SNum(..), SNat(..))
import Data.Singletons.TypeLits (withKnownNat)
#endif
#endif
import Math.VectorSpace.Dual
import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
import Data.Monoid.Additive
import Data.Void
import Linear (V0, V1, V2, V3, V4)
import qualified Linear.Affine as LinAff

import Control.Applicative
import Control.Arrow

import qualified GHC.Generics as Gnrx
import GHC.Generics (Generic, (:*:)(..))
import Data.Kind (Type)
import Proof.Propositional (Empty(..))

import Data.CallStack (HasCallStack)



interiorSemimanifoldWitness :: ∀ a . SemimanifoldWithBoundary a
          => SemimanifoldWitness (Interior a)
interiorSemimanifoldWitness = case smfdWBoundWitness @a of
  OpenManifoldWitness -> semimanifoldWitness
  SmfdWBoundWitness -> semimanifoldWitness

#define VectorSpaceSansBoundary(v, s)                         \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
                   => SemimanifoldWithBoundary (v) where {      \
  type Interior (v) = v;                                 \
  type Boundary (v) = EmptyMfd (ZeroDim s);               \
  type HalfNeedle (v) = ℝay;                             \
  smfdWBoundWitness = OpenManifoldWitness;                \
  fromInterior = id;                                     \
  fromBoundary b = case b of {};                          \
  separateInterior = Right;                              \
  p|+^_ = case p of {};                                   \
  a.+^|b = Right $ a^+^b;                                \
  extendToBoundary _ _ = Nothing };                       \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
                  => PseudoAffineWithBoundary (v) where {\
  _!-|p = case p of {};                                   \
  (.--!) = (-) };                                        \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
                => ProjectableBoundary (v) where {              \
  projectToBoundary _ p = case p of {};                  \
  marginFromBoundary p = case p of {} }

VectorSpaceSansBoundary(ℝ,ℝ)
VectorSpaceSansBoundary(V0 s, s)
VectorSpaceSansBoundary(V1 s, s)
VectorSpaceSansBoundary(V2 s, s)
VectorSpaceSansBoundary(V3 s, s)
VectorSpaceSansBoundary(V4 s, s)

data ProductBoundary a b
  = BoundOfL !(Boundary a) !(Interior b)
  | BoundOfR !(Interior a) !(Boundary b)

data ProductBoundaryNeedleT (dn :: Dualness) a b v
  = ZeroProductBoundaryNeedle
  | NBoundOfL !(dn`Space`Needle (Boundary a)) !(dn`Space`Needle (Interior b)) !v
  | NBoundOfR !(dn`Space`Needle (Interior a)) !(dn`Space`Needle (Boundary b)) !v
type ProductBoundaryNeedle a b = ProductBoundaryNeedleT Vector a b
                                     (Scalar (Needle (Interior a)))

instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Interior b))
         , AdditiveGroup (dn`Space`Needle (Interior a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , AdditiveGroup v
         , ValidDualness dn )
    => AffineSpace (ProductBoundaryNeedleT dn a b v) where
  type Diff (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
  ZeroProductBoundaryNeedle .+^ n = n
  n .+^ ZeroProductBoundaryNeedle = n
  NBoundOfL x y v .+^ NBoundOfL ξ υ β = NBoundOfL (x^+^ξ) (y^+^υ) (v^+^β)
  NBoundOfR x y v .+^ NBoundOfR ξ υ β = NBoundOfR (x^+^ξ) (y^+^υ) (v^+^β)
  n .-. ZeroProductBoundaryNeedle = n
  NBoundOfL x y v .-. NBoundOfL ξ υ β = NBoundOfL (x^-^ξ) (y^-^υ) (v^-^β)
  NBoundOfR x y v .-. NBoundOfR ξ υ β = NBoundOfR (x^-^ξ) (y^-^υ) (v^-^β)

instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Interior b))
         , AdditiveGroup (dn`Space`Needle (Interior a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , AdditiveGroup v
         , ValidDualness dn )
    => AdditiveGroup (ProductBoundaryNeedleT dn a b v) where
  zeroV = ZeroProductBoundaryNeedle
  (^+^) = (.+^)
  negateV ZeroProductBoundaryNeedle = ZeroProductBoundaryNeedle
  negateV (NBoundOfL x y v) = NBoundOfL (negateV x) (negateV y) (negateV v)
  negateV (NBoundOfR x y v) = NBoundOfR (negateV x) (negateV y) (negateV v)

instance ∀ a b v dn .
         ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar VectorSpace
           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn )
    => VectorSpace (ProductBoundaryNeedleT dn a b v) where
  type Scalar (ProductBoundaryNeedleT dn a b v) = Scalar v
  (*^) = boundaryHasSameScalar @a (boundaryHasSameScalar @b (
            case (decideDualness @dn, smfdWBoundWitness @a, smfdWBoundWitness @b) of
     (VectorWitness, _, _) -> \μ -> \case
        ZeroProductBoundaryNeedle -> ZeroProductBoundaryNeedle
        NBoundOfL x y v -> NBoundOfL (μ*^x) (μ*^y) (μ*^v)
        NBoundOfR x y v -> NBoundOfR (μ*^x) (μ*^y) (μ*^v)
     (FunctionalWitness, SmfdWBoundWitness, SmfdWBoundWitness)
                       -> case ( dualSpaceWitness @(Needle (Interior a))
                               , dualSpaceWitness @(Needle (Boundary a))
                               , dualSpaceWitness @(Needle (Interior b))
                               , dualSpaceWitness @(Needle (Boundary b)) ) of
       (DualSpaceWitness, DualSpaceWitness, DualSpaceWitness, DualSpaceWitness)
            -> \μ -> \case
        ZeroProductBoundaryNeedle -> ZeroProductBoundaryNeedle
        NBoundOfL x y v -> NBoundOfL (μ*^x) (μ*^y) (μ*^v)
        NBoundOfR x y v -> NBoundOfR (μ*^x) (μ*^y) (μ*^v)
    ))

#if MIN_VERSION_linearmap_category(0,6,0)
type family ProductBoundaryNeedleTDimension dna dnb dv where
  ProductBoundaryNeedleTDimension 
    ('Just n) ('Just m) ('Just o) = 'Just (n*m*o - 1)
  ProductBoundaryNeedleTDimension _ _ _ = 'Nothing

instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn )
    => DimensionAware (ProductBoundaryNeedleT dn a b v) where
  type StaticDimension (ProductBoundaryNeedleT dn a b v)
          = ProductBoundaryNeedleTDimension (StaticDimension (dn`Space`Needle (Interior a)))
                                            (StaticDimension (dn`Space`Needle (Interior b)))
                                            (StaticDimension v)
  dimensionalityWitness = case ( interiorSemimanifoldWitness @a
                               , interiorSemimanifoldWitness @b ) of
      (SemimanifoldWitness, SemimanifoldWitness)
                -> case ( dimensionality @(dn`Space`Needle (Interior a))
                        , dimensionality @(dn`Space`Needle (Interior b))
                        , dimensionality @v ) of
       (StaticDimensionalCase, StaticDimensionalCase, StaticDimensionalCase)
            -> withKnownNat (dimensionalitySing @(dn`Space`Needle (Interior a))
                               %* dimensionalitySing @(dn`Space`Needle (Interior b))
                               %* dimensionalitySing @v
                               %- SNat @1
                            )
                IsStaticDimensional
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , n`Dimensional`(dn`Space`Needle (Interior a))
         , m`Dimensional`(dn`Space`Needle (Interior b))
         , o`Dimensional`v
         , KnownNat d, d ~ (n*m*o-1)
         , ValidDualness dn )
    => d`Dimensional`(ProductBoundaryNeedleT dn a b v) where
#endif

instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn )
    => TensorSpace (ProductBoundaryNeedleT dn a b v) where
  type TensorProduct (ProductBoundaryNeedleT dn a b v) w
          = ProductBoundaryNeedleT dn a b (v⊗w)
  wellDefinedVector ZeroProductBoundaryNeedle = Just ZeroProductBoundaryNeedle
  wellDefinedTensor t@(Tensor ZeroProductBoundaryNeedle) = Just t
  
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
            '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn
         )
    => LinearSpace (ProductBoundaryNeedleT dn a b v) where
  type DualVector (ProductBoundaryNeedleT dn a b v)
         = ProductBoundaryNeedleT (Dual dn) a b (DualVector v)
  

instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
            '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn
         )
    => Semimanifold (ProductBoundaryNeedleT dn a b v) where
  type Needle (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
  (.+~^) = (^+^)
  semimanifoldWitness = SemimanifoldWitness
  
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
            '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , ValidDualness dn
         )
    => PseudoAffine (ProductBoundaryNeedleT dn a b v) where
  p.-~.q = pure (p^-^q)
  (.-~!) = (^-^)
  
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
         , SameScalar LinearSpace
            '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
         , AdditiveGroup (dn`Space`Needle (Boundary a))
         , AdditiveGroup (dn`Space`Needle (Boundary b))
         , OpenManifold (Scalar v)
         , ValidDualness dn
         )
    => SemimanifoldWithBoundary (ProductBoundaryNeedleT dn a b v) where
  type Interior (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
  type Boundary (ProductBoundaryNeedleT dn a b v) = EmptyMfd v
  type HalfNeedle (ProductBoundaryNeedleT dn a b v) = ℝay
  smfdWBoundWitness = OpenManifoldWitness

instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
                 , SameScalar LinearSpace
                    '[ Needle (Interior a), Needle (Interior b) ]
                 , Num' (Scalar (Needle (Interior a)))
                 )
   => Semimanifold (ProductBoundary a b) where
  type Needle (ProductBoundary a b) = ProductBoundaryNeedle a b
--ProductBoundary x y.+~^(δx, δy)
--     = case (separateInterior x, separateInterior y) of
-- (Left bx, Right _) -> case y .+^| δy of
--            Right iy' -> undefined
  (.+~^) = undefined
  semimanifoldWitness = case ( semimanifoldWitness @(Interior a)
                             , semimanifoldWitness @(Interior b) ) of
    (SemimanifoldWitness, SemimanifoldWitness)
       -> undefined -- SemimanifoldWitness

instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
                 , SameScalar LinearSpace
                    '[ Needle (Interior a), Needle (Interior b) ]
                 , Num' (Scalar (Needle (Interior a)))
                 )
   => PseudoAffine (ProductBoundary a b) where
  p.-~!q = case p.-~.q of
             Just v -> v
             Nothing -> error "No path found in product-space boundary."
  (.-~.) = case ( pseudoAffineWitness @(Interior a)
                , pseudoAffineWitness @(Interior b) ) of
   (PseudoAffineWitness SemimanifoldWitness, PseudoAffineWitness SemimanifoldWitness)
    -> let BoundOfL bx y − BoundOfL bξ υ
             = case (bx.-~.bξ, fromInterior @b y.--.fromInterior υ) of
                 (Just δbx, Just δy) -> Just $ NBoundOfL δbx δy 1
                 (_, Nothing) -> Nothing
           BoundOfL bx y − BoundOfR ξ bυ
             = case ( fromBoundary @a bx.--.fromInterior ξ
                    , projectToBoundary (fromInterior @b y) bυ ) of
                 (Just δbx, Just (δby, dy))
                    -> Just $ NBoundOfR (δbx^*(1+dy)) δby 1
                 _ -> Nothing
       in (−)
  pseudoAffineWitness = case ( pseudoAffineWitness @(Interior a)
                             , pseudoAffineWitness @(Interior b) ) of
    (PseudoAffineWitness SemimanifoldWitness
     , PseudoAffineWitness SemimanifoldWitness)
       -> undefined {- PseudoAffineWitness SemimanifoldWitness -}

instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
                 , SameScalar LinearSpace
                    '[ Needle (Interior a), Needle (Interior b)
                     , FullSubspace (HalfNeedle a)
                     ]
                 , RealFrac'' (Scalar (Needle (Interior a)))
                 )
   => SemimanifoldWithBoundary (ProductBoundary a b) where
  type Interior (ProductBoundary a b) = ProductBoundary a b
  type Boundary (ProductBoundary a b) = EmptyMfd (Needle (Boundary a), Needle (Boundary b))
  type HalfNeedle (ProductBoundary a b) = (HalfNeedle a, Needle (Boundary b))
  q|+^_ = case q of {}
  p.+^|q = Right $ p.+~^q
  fromInterior = id
  fromBoundary q = case q of {}
  smfdWBoundWitness = boundaryHasSameScalar @a
     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness -> OpenManifoldWitness)
  needleIsOpenMfd r = needleIsOpenMfd @a (needleIsOpenMfd @b
                        (case closedScalarWitness @(Scalar (Needle (Interior a))) of
                           ClosedScalarWitness -> r))
  extendToBoundary q = case q of {}
  scalarIsOpenMfd r = boundaryHasSameScalar @a
     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness -> r)
  boundaryHasSameScalar r = boundaryHasSameScalar @a (boundaryHasSameScalar @b
     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness -> r))

instance (Empty (Boundary a), Empty (Boundary b)) => Empty (ProductBoundary a b) where
  eliminate (BoundOfL ba _) = eliminate ba
  eliminate (BoundOfR _ bb) = eliminate bb

data ProductHalfNeedle a b
  = ProductHalfNeedle !(Needle (Interior a)) !(Needle (Interior b))

instance (AdditiveGroup (Needle (Interior a)), AdditiveGroup (Needle (Interior b)))
             => AdditiveMonoid (ProductHalfNeedle a b) where
  zeroHV = ProductHalfNeedle zeroV zeroV
  addHVs (ProductHalfNeedle v w) (ProductHalfNeedle ϋ ĥ)
            = ProductHalfNeedle (v^+^ϋ) (w^+^ĥ)
instance ( SemimanifoldWithBoundary a
         , SameScalar VectorSpace
            '[ Needle (Interior a), Needle (Interior b) ]
         , RealFrac'' (Scalar (Needle (Interior a)))
         ) => HalfSpace (ProductHalfNeedle a b) where
  type FullSubspace (ProductHalfNeedle a b) = ProductBoundaryNeedle a b
  type Ray (ProductHalfNeedle a b) = ℝay_ (Scalar (Needle (Interior a)))
  type MirrorJoin (ProductHalfNeedle a b) = (Needle (Interior a), Needle (Interior b))
  scaleNonNeg = case smfdWBoundWitness @a of
     SmfdWBoundWitness 
        -> boundaryHasSameScalar @a (\(Cℝay μ Origin) (ProductHalfNeedle v w)
         -> ProductHalfNeedle (μ*^v) (μ*^w))
  fromFullSubspace ZeroProductBoundaryNeedle = zeroHV
  fullSubspaceIsVectorSpace q = undefined
  projectToFullSubspace = undefined
  rayIsHalfSpace _ = undefined
  fromPositiveHalf = undefined
  fromNegativeHalf = undefined

instance ∀ a b .
         ( ProjectableBoundary a, ProjectableBoundary b
         , SameScalar LinearSpace
            '[ Needle (Interior a), Needle (Interior b)
             ]
         , RealFrac'' (Scalar (Needle (Interior a)))
         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
         ) => SemimanifoldWithBoundary (a,b) where
  type Interior (a,b) = (Interior a, Interior b)
  type Boundary (a,b) = ProductBoundary a b
  type HalfNeedle (a,b) = ProductHalfNeedle a b
  extendToBoundary = undefined
  smfdWBoundWitness = case (smfdWBoundWitness @a, smfdWBoundWitness @b) of
    (OpenManifoldWitness, OpenManifoldWitness)
        -> needleIsOpenMfd @a (needleIsOpenMfd @b (
             boundaryHasSameScalar @(Needle a) (boundaryHasSameScalar @(Needle b)
               (case (semimanifoldWitness @(Interior a), semimanifoldWitness @(Interior b))
                 of (SemimanifoldWitness, SemimanifoldWitness)
                        -> needleBoundaryIsTriviallyProjectible @a
                            (needleBoundaryIsTriviallyProjectible @b OpenManifoldWitness) )
            )))
    (SmfdWBoundWitness, SmfdWBoundWitness)
        -> boundaryHasSameScalar @a
            (boundaryHasSameScalar @b
              (needleIsOpenMfd @(Interior a)
                (needleIsOpenMfd @(Interior b)
                  (case ( semimanifoldWitness @(Interior a)
                        , semimanifoldWitness @(Interior b)
                        , closedScalarWitness @(Scalar (Needle (Interior a)))
                        )
                 of (SemimanifoldWitness, SemimanifoldWitness, ClosedScalarWitness)
                        -> needleBoundaryIsTriviallyProjectible @a
                            (needleBoundaryIsTriviallyProjectible @b
                              (boundaryHasSameScalar @(Needle (Interior a))
                                (boundaryHasSameScalar @(Needle (Interior b))
                                  SmfdWBoundWitness)))))))
  boundaryHasSameScalar q = undefined
  needleIsOpenMfd _ = undefined

instance ∀ a b .
         ( ProjectableBoundary a, ProjectableBoundary b
         , SameScalar LinearSpace
            '[ Needle (Interior a), Needle (Interior b)
             , Needle (Boundary a), Needle (Boundary b)
             ]
         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
         , RealFrac'' (Scalar (Needle (Interior a)))
         ) => PseudoAffineWithBoundary (a,b) where

instance ∀ a b .
         ( ProjectableBoundary a, ProjectableBoundary b
         , SameScalar LinearSpace
            '[ Needle (Interior a), Needle (Interior b)
             , Needle (Boundary a), Needle (Boundary b)
             ]
         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
         , RealFrac'' (Scalar (Needle (Interior a)))
         ) => ProjectableBoundary (a,b) where
  needleBoundaryIsTriviallyProjectible q
      = needleBoundaryIsTriviallyProjectible @a
         (needleBoundaryIsTriviallyProjectible @b
           (boundaryHasSameScalar @(Needle (Interior a))
             (boundaryHasSameScalar @(Needle (Interior b))
               (needleIsOpenMfd @a
                 (needleIsOpenMfd @b
                   (case (semimanifoldWitness @(Interior a), semimanifoldWitness @(Interior b))
                     of (SemimanifoldWitness, SemimanifoldWitness) -> q))))))

instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S⁰_ s) where
  type Interior (S⁰_ s) = S⁰_ s
  type Boundary (S⁰_ s) = EmptyMfd (ZeroDim s)
  type HalfNeedle (S⁰_ s) = ZeroDim s
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  NegativeHalfSphere .+^| Origin = Right NegativeHalfSphere
  PositiveHalfSphere .+^| Origin = Right PositiveHalfSphere
  extendToBoundary _ _ = Nothing
  smfdWBoundWitness = OpenManifoldWitness

instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S¹_ s) where
  type Interior (S¹_ s) = (S¹_ s)
  type Boundary (S¹_ s) = EmptyMfd (ZeroDim s)
  type HalfNeedle (S¹_ s) = ℝay_ s
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  _ .+^| p = case p of {}
  extendToBoundary _ _ = Nothing
  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> OpenManifoldWitness
  scalarIsOpenMfd q = case closedScalarWitness @s of ClosedScalarWitness -> q
  boundaryHasSameScalar q = case closedScalarWitness @s of ClosedScalarWitness -> q

instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S¹_ s) where
  _!-|p = case p of {}
  (.--!) = (.-~!)

instance ∀ s . RealFloat'' s => ProjectableBoundary (S¹_ s) where
  scalarBoundaryIsTriviallyProjectible q = case closedScalarWitness @s of
     ClosedScalarWitness -> q
  projectToBoundary _ p = case p of {}
  marginFromBoundary p = case p of {}

instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S²_ s) where
  type Interior (S²_ s) = S²_ s
  type Boundary (S²_ s) = EmptyMfd s
  type HalfNeedle (S²_ s) = ℝay_ s
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  _ .+^| p = case p of {}
  extendToBoundary _ _ = Nothing
  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> OpenManifoldWitness
  scalarIsOpenMfd q = case closedScalarWitness @s of ClosedScalarWitness -> q
  boundaryHasSameScalar q = case closedScalarWitness @s of ClosedScalarWitness -> q

instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S²_ s) where
  _!-|p = case p of {}
  (.--!) = (.-~!)

instance ∀ s . RealFloat'' s => ProjectableBoundary (S²_ s) where
  scalarBoundaryIsTriviallyProjectible q = case closedScalarWitness @s of
     ClosedScalarWitness -> q
  projectToBoundary _ p = case p of {}
  marginFromBoundary p = case p of {}


instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (D¹_ s) where
  type Interior (D¹_ s) = s
  type Boundary (D¹_ s) = (S⁰_ s)
  type HalfNeedle (D¹_ s) = ℝay_ s
  fromBoundary NegativeHalfSphere = D¹ (-1)
  fromBoundary PositiveHalfSphere = D¹ 1
  fromInterior = D¹ . tanh
  separateInterior (D¹ (-1)) = Left NegativeHalfSphere
  separateInterior (D¹ 1) = Left PositiveHalfSphere
  separateInterior (D¹ x) = Right $ atanh x
  NegativeHalfSphere|+^Cℝay l Origin = D¹ $ 1 - 4/(l+2)
  PositiveHalfSphere|+^Cℝay l Origin = D¹ $ 4/(l+2) - 1
  (.+^|) = case (linearManifoldWitness @s, closedScalarWitness @s) of
   (LinearManifoldWitness, ClosedScalarWitness) ->
    let addBD¹ (D¹ p) l
          | p' >= 1    = Left (PositiveHalfSphere, (p'-1) / l)
          | p' <= -1   = Left (NegativeHalfSphere, (p'+1) / l)
          | otherwise  = Right $ atanh p'
         where p' = p+l
    in addBD¹
  extendToBoundary = case (linearManifoldWitness @s, closedScalarWitness @s) of
   (LinearManifoldWitness, ClosedScalarWitness) ->
    let e2b _ dir
         | dir > 0    = Just PositiveHalfSphere
         | dir < 0    = Just NegativeHalfSphere
         | otherwise  = Nothing
    in e2b
  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> SmfdWBoundWitness
  scalarIsOpenMfd q = case (closedScalarWitness @s, linearManifoldWitness @s) of
   (ClosedScalarWitness, LinearManifoldWitness) -> q
  boundaryHasSameScalar q = case (closedScalarWitness @s, linearManifoldWitness @s) of
   (ClosedScalarWitness, LinearManifoldWitness) -> q
  needleIsOpenMfd q = case (closedScalarWitness @s, linearManifoldWitness @s) of
   (ClosedScalarWitness, LinearManifoldWitness) -> q


instance ( Num' n, OpenManifold n, LinearManifold (a n)
         , Scalar (a n) ~ n, Needle (a n) ~ a n )
            => SemimanifoldWithBoundary (LinAff.Point a n) where
  type Boundary (LinAff.Point a n) = EmptyMfd (ZeroDim n)
  type Interior (LinAff.Point a n) = LinAff.Point a n
  type HalfNeedle (LinAff.Point a n) = ℝay
  smfdWBoundWitness = OpenManifoldWitness
  LinAff.P p.+^|v = Right . LinAff.P $ p^+^v
  fromInterior = id
  fromBoundary b = case b of {}
  b|+^_ = case b of {}

instance ( Num' n, OpenManifold n, LinearManifold (a n)
         , Scalar (a n) ~ n, Needle (a n) ~ a n )
            => PseudoAffineWithBoundary (LinAff.Point a n) where
  LinAff.P p.--!LinAff.P q = p^-^q
  _!-|b = case b of {}

instance ∀ n a .  ( Num' n, OpenManifold n, LinearManifold (a n), ProjectableBoundary n
                  , Scalar (a n) ~ n, Needle (a n) ~ a n )
            => ProjectableBoundary (LinAff.Point a n) where
  projectToBoundary _ b = case b of {}
  marginFromBoundary b _ = case b of {}

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => SemimanifoldWithBoundary (Tensor s v w) where
  type Interior (Tensor s v w) = (Tensor s v w)
  type Boundary (Tensor s v w) = EmptyMfd (ZeroDim s)
  type HalfNeedle (Tensor s v w) = ℝay_ s
  smfdWBoundWitness = OpenManifoldWitness
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  a.+^|b = Right $ a^+^b
  extendToBoundary _ _ = Nothing

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => PseudoAffineWithBoundary (Tensor s v w) where
  _!-|p = case p of {}
  (.--!) = (^-^)

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => SemimanifoldWithBoundary (LinearMap s v w) where
  type Interior (LinearMap s v w) = (LinearMap s v w)
  type Boundary (LinearMap s v w) = EmptyMfd (ZeroDim s)
  type HalfNeedle (LinearMap s v w) = ℝay
  smfdWBoundWitness = OpenManifoldWitness
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  a.+^|b = Right $ a^+^b
  extendToBoundary _ _ = Nothing

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s, ProjectableBoundary s
         ) => ProjectableBoundary (LinearMap s v w) where
  projectToBoundary _ p = case p of {}
  marginFromBoundary p = case p of {}

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => PseudoAffineWithBoundary (LinearMap s v w) where
  _!-|p = case p of {}
  (.--!) = (^-^)

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => SemimanifoldWithBoundary (LinearFunction s v w) where
  type Interior (LinearFunction s v w) = (LinearFunction s v w)
  type Boundary (LinearFunction s v w) = EmptyMfd (ZeroDim s)
  type HalfNeedle (LinearFunction s v w) = ℝay
  smfdWBoundWitness = OpenManifoldWitness
  fromInterior = id
  fromBoundary b = case b of {}
  separateInterior = Right
  p|+^_ = case p of {}
  a.+^|b = Right $ a^+^b
  extendToBoundary _ _ = Nothing

instance ( LinearSpace v, LinearSpace w
         , s ~ Scalar v, s ~ Scalar w
         , Num' s, OpenManifold s
         ) => PseudoAffineWithBoundary (LinearFunction s v w) where
  _!-|p = case p of {}
  (.--!) = (^-^)



instance ( Semimanifold a
         , Semimanifold (VRep a), Needle a ~ GenericNeedle a
         , OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
         , LinearSpace (Needle (Gnrx.Rep a Void))
         , Num' (Scalar (Needle (Gnrx.Rep a Void))) )
            => SemimanifoldWithBoundary (GenericNeedle a) where
  type Interior (GenericNeedle a) = GenericNeedle a
  type Boundary (GenericNeedle a) = EmptyMfd (ZeroDim (Scalar (Needle (Gnrx.Rep a Void))))
  type HalfNeedle (GenericNeedle a) = ℝay_ (Scalar (Needle (Gnrx.Rep a Void)))
  extendToBoundary _ _ = Nothing
  smfdWBoundWitness = OpenManifoldWitness
  needleIsOpenMfd q = q
  scalarIsOpenMfd q = q
  boundaryHasSameScalar q = q
  b|+^_ = case b of {}
  p .+^| k = Right $ p^+^k
  fromBoundary b = case b of {}


instance ( Semimanifold a
         , Semimanifold (VRep a), Needle a ~ GenericNeedle a
         , OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
         , LinearSpace (Needle (Gnrx.Rep a Void))
         , Num' (Scalar (Needle (Gnrx.Rep a Void))) )
            => PseudoAffineWithBoundary (GenericNeedle a) where
  _ !-| b = case b of {}
  (.--!) = (^-^)