content: {-# LANGUAGE TypeFamilies, MonoLocalBinds #-}
  module T12526 where
  
  import Data.Kind (Type)
  
  type family P (s :: Type -> Type) :: Type -> Type -> Type
  type instance P Signal = Causal
  
  type family S (p :: Type -> Type -> Type) :: Type -> Type
  type instance S Causal = Signal
  
  class (P (S p) ~ p) => CP p
  instance CP Causal
  
  data Signal a = Signal
  data Causal a b = Causal
  
  shapeModOsci :: CP p => p Float Float
  shapeModOsci = undefined
  
  f :: Causal Float Float -> Bool
  f = undefined
  
  -- This fails
  ping :: Bool
  ping = let osci = shapeModOsci in  f osci
  
  
  -- This works
  -- ping :: Bool
  -- ping = f shapeModOsci
  
  
  {-
  
      osci :: p Float Float
      [W] CP p, [D] P (S p) ~ p
  -->
      [W] CP p, [D] P fuv1 ~ fuv2, S p ~ fuv1, fuv2 ~ p
  -->
      p := fuv2
      [W] CP fuv2, [D] P fuv1 ~ fuv2, S fuv2 ~ fuv1
  
  -}
  
  -- P (S p) ~ p
  -- p Float Float ~ Causal Float Float
  
  
  {-
    P (S p) ~ p
    p Float Float ~ Causal Float Float
  
  --->
    S p ~ fuv1    (FunEq)
    P fuv1 ~ fuv2 (FunEq)
    fuv2 ~ p
    p F F ~ Causal F F
  
  --->
    p := fuv2
  
    fuv2 ~ Causal
    S fuv2 ~ fuv1 (FunEq)
    P fuv1 ~ fuv2 (FunEq)
  
  ---> unflatten
    fuv1 := S fuv2
    fuv2 := Causal
  
  -}
  