hm

typestuff.hs

data DLens :: (k -> Type) -> ((k ~> b),(b ~> k ~> k)) -> Type -> Type where 
  DLens :: forall k b
           (c :: k -> Type) 
           (g :: k ~> b) 
           (s :: b ~> k ~> k). 
          (forall f (r :: k) (x :: b) y  z. ( Functor f
                                            , y ~ (g @@ r)
                                            , z ~ ((s @@ x) @@ r)
                                            , SameKind y x -- these seem to help inference
                                            , SameKind r z)  => 
               (Sing y -> f (Sing x)) 
            -> c r 
            -> f (c z))
        -> DLens c '(g,s) b
        
dOver :: forall k b (c :: k -> Type) 
                    (g :: k ~> b) 
                    (s :: b ~> k ~> k) 
                    (f :: b -> b) . -- if we have (f :: b ~> b) it'll typecheck here but won't ever typecheck when we try to use it
         DLens c '(g,s) b 
      -> (forall (x :: b). Sing x -> Sing (f x)) 
      -> (forall (r :: k). c r -> c ( (s @@ (f  (g @@ r))) @@ r))
dOver dl@(DLens l) f = 
  let x :: forall (r :: k). c r ->  Sing (g @@ r)
      x cr = dView dl cr 

      x' :: forall (r :: k). c r -> Sing (f (g @@ r))
      x' cr = 
        let x'' = x cr 
        in f x'' 

      g :: forall (r :: k). c r -> c ( (s @@ (f  (g @@ r))) @@ r)
      g cr = 
        let y = x' cr 
        in dSet dl y cr 
  in g