> {-# LANGUAGE FlexibleContexts #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE TypeApplications #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# OPTIONS -Wno-missing-methods #-}

> module Figures where

> import Data.Type.Require
> import GHC.TypeLits
> import Data.Type.Bool
> import Data.Type.Equality
> import Data.Proxy

> data Color = RGB Nat Nat Nat

> type instance Equ (RGB r g b) (RGB r' g' b')
>   = r == r' && g == g' && b == b'

> data Dim = R2 | R3
> type instance ShowTE R2 = Text "R2"
> type instance ShowTE R3 = Text "R3"

> data family Figure (d :: Dim) (c :: Color)


> data instance Figure R2 c
>   = Circle Double Double Double -- center, radius? not important

> data instance Figure R3 c
>   = Sphere Double Double Double Double


> combine :: Figure d c -> Figure d c -> Figure d c
> combine :: Figure d c -> Figure d c -> Figure d c
combine Figure d c
f Figure d c
g = Figure d c
forall a. HasCallStack => a
undefined

combine (Circle 1 1 1) (Sphere 1 1 1 1) ->

• Couldn't match type ‘'R3’ with ‘'R2’
  Expected type: Figure 'R2 c
  Actual type: Figure 'R3 c


> data OpEqDim  (d :: Dim)  (d' :: Dim)
> data OpEqDim' (b :: Bool) (d :: Dim)   (d' :: Dim)
> data OpEqCol  (c :: Color) (c' :: Color)
> data OpEqCol' (b :: Bool) (c :: Color) (c' :: Color)

> data OpCombine d d' c c' where
>   OpCombine :: Figure d c -> Figure d' c' -> OpCombine d d' c c'

> instance
>   ( Require (OpEqDim d d') ctx
>   , Require (OpEqCol c c') ctx
>   )
>   =>
>   Require (OpCombine d d' c c') ctx where
>   type ReqR (OpCombine d d' c c') =
>     Figure d c
>   req :: Proxy ctx -> OpCombine d d' c c' -> ReqR (OpCombine d d' c c')
req Proxy ctx
ctx (OpCombine Figure d c
f Figure d' c'
g) =
>     ReqR (OpCombine d d' c c')
forall a. HasCallStack => a
undefined

> instance
>   (Require (OpEqDim' (d == d') d d')) ctx
>   =>
>   Require (OpEqDim d d') ctx where
>   type ReqR (OpEqDim d d') = ReqR (OpEqDim' (d == d') d d')

> instance Require (OpEqDim' 'True  d d') ctx where {}

> instance
>   Require (OpError
>   (Text "Dimensional error:" :$$: Text "cannot combine figure of dimension "
>   :<>: ShowTE d :<>: Text " and dimension " :<>: ShowTE d')) ctx
>   => Require (OpEqDim' 'False d d') ctx


> instance
>   (Require (OpEqCol' (Equ c c') c c')) ctx
>   =>
>   Require (OpEqCol c c') ctx where
>   type ReqR (OpEqCol c c') = ReqR (OpEqCol' (Equ c c') c c')

> instance Require (OpEqCol' 'True  c c') ctx where {}


an sloppy error:

> instance
>   Require (OpError
>   (Text "Error, combined images must be of the same color")) ctx
>   => Require (OpEqCol' 'False c c') ctx


> combine' :: Figure d c -> Figure d' c' -> ReqR (OpCombine d d' c c')
combine' Figure d c
f Figure d' c'
f' = Proxy '[ 'Text "combining"]
-> OpCombine d d' c c' -> ReqR (OpCombine d d' c c')
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req (Proxy '[ 'Text "combining"]
forall k (t :: k). Proxy t
Proxy @( '[ Text "combining"] )) (Figure d c -> Figure d' c' -> OpCombine d d' c c'
forall (d :: Dim) (c :: Color) (d' :: Dim) (c' :: Color).
Figure d c -> Figure d' c' -> OpCombine d d' c c'
OpCombine Figure d c
f Figure d' c'
f')

combine' (Circle 1 1 1) (Sphere 1 1 1 1) ->

• Error: Dimensional error:
         cannot combine figure of dimension R2 and dimension R3
  trace: combining..



combine' (Circle 1 1 1 :: Figure R2 (RGB 1 1 1))
         (Circle 1 1 1 :: Figure R2 (RGB 1 1 2)) ->

• Error: Error, combined images must be of the same color
  trace: combining..

> f1 :: Figure 'R2 ('RGB 1 1 1)
f1 = (Double -> Double -> Double -> Figure 'R2 ('RGB 1 1 1)
forall (c :: Color). Double -> Double -> Double -> Figure 'R2 c
Circle Double
2 Double
2 Double
2 :: Figure R2 (RGB 1 1 1))
> f2 :: Figure 'R3 ('RGB 1 1 1)
f2 = (Double -> Double -> Double -> Double -> Figure 'R3 ('RGB 1 1 1)
forall (c :: Color).
Double -> Double -> Double -> Double -> Figure 'R3 c
Sphere Double
2 Double
2 Double
2 Double
2:: Figure R3 (RGB 1 1 1))

> f :: CFigure 'R2 ('RGB 1 1 1) ctx
f = (Proxy ctx -> Figure 'R2 ('RGB 1 1 1))
-> CFigure 'R2 ('RGB 1 1 1) ctx
forall (d :: Dim) (c :: Color) (ctx :: [ErrorMessage]).
(Proxy ctx -> Figure d c) -> CFigure d c ctx
CFigure ((Proxy ctx -> Figure 'R2 ('RGB 1 1 1))
 -> CFigure 'R2 ('RGB 1 1 1) ctx)
-> (Proxy ctx -> Figure 'R2 ('RGB 1 1 1))
-> CFigure 'R2 ('RGB 1 1 1) ctx
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
Proxy  -> Figure 'R2 ('RGB 1 1 1)
f1
> f' :: CFigure 'R3 ('RGB 1 1 1) ctx
f' = (Proxy ctx -> Figure 'R3 ('RGB 1 1 1))
-> CFigure 'R3 ('RGB 1 1 1) ctx
forall (d :: Dim) (c :: Color) (ctx :: [ErrorMessage]).
(Proxy ctx -> Figure d c) -> CFigure d c ctx
CFigure ((Proxy ctx -> Figure 'R3 ('RGB 1 1 1))
 -> CFigure 'R3 ('RGB 1 1 1) ctx)
-> (Proxy ctx -> Figure 'R3 ('RGB 1 1 1))
-> CFigure 'R3 ('RGB 1 1 1) ctx
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
Proxy -> Figure 'R3 ('RGB 1 1 1)
f2

> f'' :: CFigure 'R3 ('RGB 1 1 1) ('Text "tracefig!!!!!" : ctx)
f'' = (Proxy ('Text "tracefig!!!!!" : ctx) -> Proxy ctx)
-> CFigure 'R3 ('RGB 1 1 1) ctx
-> CFigure 'R3 ('RGB 1 1 1) ('Text "tracefig!!!!!" : ctx)
forall (ctx' :: [ErrorMessage]) (ctx :: [ErrorMessage]) (d :: Dim)
       (c :: Color).
(Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
traceFig
>    (\(Proxy ('Text "tracefig!!!!!" : ctx)
_ :: Proxy (Text "tracefig!!!!!" : ctx)) -> Proxy ctx
forall k (t :: k). Proxy t
Proxy :: Proxy ctx ) (CFigure 'R3 ('RGB 1 1 1) ctx
 -> CFigure 'R3 ('RGB 1 1 1) ('Text "tracefig!!!!!" : ctx))
-> CFigure 'R3 ('RGB 1 1 1) ctx
-> CFigure 'R3 ('RGB 1 1 1) ('Text "tracefig!!!!!" : ctx)
forall a b. (a -> b) -> a -> b
$ CFigure 'R3 ('RGB 1 1 1) ctx
forall (ctx :: [ErrorMessage]). CFigure 'R3 ('RGB 1 1 1) ctx
f'

> tr :: CFigure d c ('Text "tracefig!!!!!" : ctx) -> CFigure d c ctx
tr = (Proxy ctx -> Proxy ('Text "tracefig!!!!!" : ctx))
-> CFigure d c ('Text "tracefig!!!!!" : ctx) -> CFigure d c ctx
forall (ctx' :: [ErrorMessage]) (ctx :: [ErrorMessage]) (d :: Dim)
       (c :: Color).
(Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
traceFig
>    (\(Proxy ctx
_ :: Proxy (ctx)) -> Proxy ('Text "tracefig!!!!!" : ctx)
forall k (t :: k). Proxy t
Proxy :: Proxy (Text "tracefig!!!!!" : ctx) )

> data CFigure d c (ctx :: [ErrorMessage])
>  = CFigure {CFigure d c ctx -> Proxy ctx -> Figure d c
mkCFig :: Proxy ctx -> Figure d c}


> combine''
>   :: (Require (OpEqDim' (d == d') d d') (Text "lalo" :ctx),
>       Require (OpEqCol' (Equ c c') c c') (Text "lalo" : ctx)) =>
>      CFigure d c ctx -> CFigure d' c' ctx -> CFigure d c ctx
> combine'' :: CFigure d c ctx -> CFigure d' c' ctx -> CFigure d c ctx
combine'' (CFigure Proxy ctx -> Figure d c
f1) (CFigure Proxy ctx -> Figure d' c'
f2)
>   = (Proxy ctx -> Figure d c) -> CFigure d c ctx
forall (d :: Dim) (c :: Color) (ctx :: [ErrorMessage]).
(Proxy ctx -> Figure d c) -> CFigure d c ctx
CFigure ((Proxy ctx -> Figure d c) -> CFigure d c ctx)
-> (Proxy ctx -> Figure d c) -> CFigure d c ctx
forall a b. (a -> b) -> a -> b
$ \(Proxy ctx
a :: Proxy ctx) ->
>           Proxy ('Text "lalo" : ctx)
-> OpCombine d d' c c' -> ReqR (OpCombine d d' c c')
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req (Proxy ('Text "lalo" : ctx)
forall k (t :: k). Proxy t
Proxy :: Proxy (Text "lalo" : ctx))
>               (Figure d c -> Figure d' c' -> OpCombine d d' c c'
forall (d :: Dim) (c :: Color) (d' :: Dim) (c' :: Color).
Figure d c -> Figure d' c' -> OpCombine d d' c c'
OpCombine (Proxy ctx -> Figure d c
f1 Proxy ctx
a) (Proxy ctx -> Figure d' c'
f2 Proxy ctx
a))


> traceFig :: (Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
> traceFig :: (Proxy ctx' -> Proxy ctx) -> CFigure d c ctx -> CFigure d c ctx'
traceFig Proxy ctx' -> Proxy ctx
fctx (CFigure Proxy ctx -> Figure d c
f) = (Proxy ctx' -> Figure d c) -> CFigure d c ctx'
forall (d :: Dim) (c :: Color) (ctx :: [ErrorMessage]).
(Proxy ctx -> Figure d c) -> CFigure d c ctx
CFigure ((Proxy ctx' -> Figure d c) -> CFigure d c ctx')
-> (Proxy ctx' -> Figure d c) -> CFigure d c ctx'
forall a b. (a -> b) -> a -> b
$ Proxy ctx -> Figure d c
f (Proxy ctx -> Figure d c)
-> (Proxy ctx' -> Proxy ctx) -> Proxy ctx' -> Figure d c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ctx' -> Proxy ctx
fctx



Error:

 > g = combine'' (tr $ tr f) (tr $ tr f'') -- (tr $ tr $ tr $ combine'' f f) f''