start using type-family-based GArrow classes

diff --git a/examples/Demo.hs b/examples/Demo.hs
index 74bbef0..fea2dc7 100644 (file)
--- a/examples/Demo.hs
+++ b/examples/Demo.hs
@@ -5,6 +5,5 @@ import GHC.HetMet.Private
 import GArrowTikZ
 
 foo x = <[ ~~x ]>
-foo' = unG . pga_flatten . foo . pga_unflatten
---foo x z = <[ let y = ~~x in ~~z y y ]>
-main = tikz (foo' (PGArrowD { unG = TikZ_const 12 }))
+
+main = tikz' $ pga_flatten . foo . pga_unflatten

diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs
index f545937..db21658 100644 (file)
--- a/examples/GArrowTikZ.hs
+++ b/examples/GArrowTikZ.hs
@@ -1,5 +1,5 @@
-{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances #-}
-module GArrowTikZ (tikz, GArrowTikZ(..))
+{-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -XNoMonoPatBinds -XKindSignatures -XGADTs -XFlexibleContexts -XFlexibleInstances -XTypeOperators -XUndecidableInstances -XTypeFamilies #-}
+module GArrowTikZ (tikz, tikz', GArrowTikZ(..))
 where
 import Prelude hiding ( id, (.), lookup )
 import Control.Category
@@ -7,7 +7,7 @@ import GHC.HetMet.GArrow
 import Data.List hiding (lookup, insert)
 import Data.Map hiding (map, (!))
 import Unify
-
+import GHC.HetMet.Private
 
 {-
 TO DO:
@@ -128,7 +128,11 @@ instance GArrowLoop GArrowTikZ (**) () where
   ga_loopl     = TikZ_loopl
   ga_loopr     = TikZ_loopr
 
-instance GArrowSTKC GArrowTikZ (,) ()
+type instance GArrowTensor      GArrowTikZ = (,)
+type instance GArrowUnit        GArrowTikZ = ()
+type instance GArrowExponent    GArrowTikZ = (->)
+
+instance GArrowSTKC GArrowTikZ
 
 
 name :: GArrowTikZ a b -> String
@@ -420,6 +424,9 @@ toTikZ' g = foldr (\x y -> x++"\\\\\n"++y) [] (map foo s)
                s = sortit (strip k)
                m = valuatit empty s
 
+tikz' :: (forall g a . PGArrow g (GArrowUnit g) a -> PGArrow g (GArrowUnit g) a) -> IO ()
+tikz' x = tikz $ unG (x (PGArrowD { unG = TikZ_const 12 }))
+main = do putStrLn "hello"
 tikz example
      = do putStrLn "\\documentclass{article}"
           putStrLn "\\usepackage[landscape,paperheight=20in,textwidth=19in]{geometry}"

diff --git a/examples/Makefile b/examples/Makefile
index 7819837..e411f32 100644 (file)
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -6,7 +6,7 @@ all:
 
 tikz:
        mkdir -p .build
-       ../../../inplace/bin/ghc-stage2 -odir .build -hidir .build GArrowTikZ.hs Unify.hs test.hs
-       ./test > .build/test.tex
+       ../../../inplace/bin/ghc-stage2 -odir .build -hidir .build GArrowTikZ.hs Unify.hs Demo.hs -o .build/demo
+       ./.build/demo > .build/test.tex
        cd .build; pdflatex test.tex
        open .build/test.pdf

diff --git a/examples/Unify.dump-coqpass b/examples/Unify.dump-coqpass
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/examples/x b/examples/x
new file mode 100644 (file)
index 0000000..48cdc1c
--- /dev/null
+++ b/examples/x
@@ -0,0 +1,1184 @@
+[3 of 3] Compiling Main             ( Demo.hs, .build/Main.o )
+
+==================== Desugared, before opt ====================
+@ co_aLI::() ~ ()
+co_aLI = TYPE ()
+
+@ co_aHe::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
+co_aHe = TYPE trans GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ co_aLI
+
+Rec {
+$dGArrowSTKC_aHd
+  :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ
+[LclId]
+$dGArrowSTKC_aHd = GArrowTikZ.$fGArrowSTKCGArrowTikZ
+
+Main.foo
+  :: forall (t_aD6 :: * -> * -> *) t_aD7.
+     <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6
+[LclId]
+Main.foo =
+  \ (@ t_aD6::* -> * -> *) (@ t_aD7) ->
+    letrec {
+      foo_aD5 :: <[t_aD7]>@t_aD6 -> <[t_aD7]>@t_aD6
+      [LclId]
+      foo_aD5 =
+        \ (x_aD4 :: <[t_aD7]>@t_aD6) ->
+          GHC.HetMet.CodeTypes.hetmet_brak
+            @ t_aD6
+            @ t_aD7
+            ((GHC.HetMet.CodeTypes.hetmet_esc @ t_aD6 @ t_aD7 x_aD4)
+             `cast` (t_aD7 :: t_aD7 ~ t_aD7)); } in
+    foo_aD5
+
+Main.foo'
+  :: forall (g_aFo :: * -> * -> *) y_aFp.
+     (GHC.HetMet.GArrow.GArrowSTKC g_aFo,
+      GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) =>
+     GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp
+[LclId]
+Main.foo' =
+  \ (@ g_aFo::* -> * -> *)
+    (@ y_aFp)
+    ($dGArrowSTKC_aFq :: GHC.HetMet.GArrow.GArrowSTKC g_aFo)
+    (@ co_aFr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()) ->
+    let {
+      @ co_aMM::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMM = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aML::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aML = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMK::() ~ ()
+      co_aMK = TYPE () } in
+    let {
+      @ co_aMJ::() ~ ()
+      co_aMJ = TYPE () } in
+    let {
+      @ co_aMI::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMH::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMH = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMG::() ~ ()
+      co_aMG = TYPE () } in
+    let {
+      @ co_aMF::() ~ ()
+      co_aMF = TYPE () } in
+    let {
+      @ co_aME::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aME = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMD::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMD = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMC::() ~ ()
+      co_aMC = TYPE () } in
+    let {
+      @ co_aMB::() ~ ()
+      co_aMB = TYPE () } in
+    let {
+      @ co_aMz::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aMz = TYPE trans co_aFr (sym co_aMB) } in
+    let {
+      @ co_aMu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aMu = TYPE trans co_aFr (sym co_aMF) } in
+    let {
+      @ co_aMp::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aMp = TYPE trans co_aFr (sym co_aMJ) } in
+    let {
+      @ co_aM1::GHC.HetMet.GArrow.GArrowUnit g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowUnit g_aFo
+      co_aM1 = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
+    let {
+      @ co_aM4::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aM4 = TYPE trans (sym co_aM1) co_aFr } in
+    let {
+      @ co_aLZ::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aLZ = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aMn::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMn = TYPE trans co_aLZ (sym co_aML) } in
+    let {
+      @ co_aMs::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMs = TYPE trans co_aLZ (sym co_aMH) } in
+    let {
+      @ co_aMx::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aMx = TYPE trans co_aLZ (sym co_aMD) } in
+    let {
+      @ co_aLV::GHC.HetMet.GArrow.GArrowUnit g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowUnit g_aFo
+      co_aLV = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
+    let {
+      @ co_aM5::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aM5 = TYPE trans (sym co_aLV) co_aFr } in
+    let {
+      @ co_aLT::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aLT = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aM6::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aM6 = TYPE trans (sym co_aLT) co_aLZ } in
+    let {
+      @ co_aLP::GHC.HetMet.GArrow.GArrowUnit g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowUnit g_aFo
+      co_aLP = TYPE GHC.HetMet.GArrow.GArrowUnit g_aFo } in
+    let {
+      @ co_aM7::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aM7 = TYPE trans (sym co_aLP) co_aFr } in
+    let {
+      @ co_aLN::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aLN = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aM8::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aM8 = TYPE trans (sym co_aLN) co_aLZ } in
+    let {
+      $dGArrowSwap_aLL
+        :: GHC.HetMet.GArrow.GArrowSwap
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrowSwap_aLL =
+        GHC.HetMet.GArrow.$p3GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
+    let {
+      $dGArrow_aM2
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrow_aM2 =
+        GHC.HetMet.GArrow.$p1GArrowSwap
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrowSwap_aLL } in
+    let {
+      $dCategory_aM3 :: Control.Category.Category g_aFo
+      [LclId]
+      $dCategory_aM3 =
+        GHC.HetMet.GArrow.$p1GArrow
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrow_aM2 } in
+    let {
+      $dGArrow_aMa
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrow_aMa =
+        $dGArrow_aM2
+        `cast` (GHC.HetMet.GArrow.T:GArrow
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4
+                :: GHC.HetMet.GArrow.T:GArrow
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrowSwap_aM9
+        :: GHC.HetMet.GArrow.GArrowSwap
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrowSwap_aM9 =
+        $dGArrowSwap_aLL
+        `cast` (GHC.HetMet.GArrow.T:GArrowSwap
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM4
+                :: GHC.HetMet.GArrow.T:GArrowSwap
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrowSwap
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrowCopy_aLK
+        :: GHC.HetMet.GArrow.GArrowCopy
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrowCopy_aLK =
+        GHC.HetMet.GArrow.$p2GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
+    let {
+      $dGArrow_aLW
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrow_aLW =
+        GHC.HetMet.GArrow.$p1GArrowCopy
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrowCopy_aLK } in
+    let {
+      $dCategory_aLX :: Control.Category.Category g_aFo
+      [LclId]
+      $dCategory_aLX =
+        GHC.HetMet.GArrow.$p1GArrow
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrow_aLW } in
+    let {
+      $dGArrow_aMd
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrow_aMd =
+        $dGArrow_aLW
+        `cast` (GHC.HetMet.GArrow.T:GArrow
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5
+                :: GHC.HetMet.GArrow.T:GArrow
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrow_aMe
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrow_aMe =
+        $dGArrow_aMd
+        `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM6 ()
+                :: GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+                     ~
+                   GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrowCopy_aMb
+        :: GHC.HetMet.GArrow.GArrowCopy
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrowCopy_aMb =
+        $dGArrowCopy_aLK
+        `cast` (GHC.HetMet.GArrow.T:GArrowCopy
+                  g_aFo co_aM6 (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                :: GHC.HetMet.GArrow.T:GArrowCopy
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrowCopy
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in
+    let {
+      $dGArrowCopy_aMc
+        :: GHC.HetMet.GArrow.GArrowCopy
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrowCopy_aMc =
+        $dGArrowCopy_aMb
+        `cast` (GHC.HetMet.GArrow.T:GArrowCopy
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM5
+                :: GHC.HetMet.GArrow.T:GArrowCopy
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrowCopy
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrowDrop_aLJ
+        :: GHC.HetMet.GArrow.GArrowDrop
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrowDrop_aLJ =
+        GHC.HetMet.GArrow.$p1GArrowSTKC @ g_aFo $dGArrowSTKC_aFq } in
+    let {
+      $dGArrow_aLQ
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrow_aLQ =
+        GHC.HetMet.GArrow.$p1GArrowDrop
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrowDrop_aLJ } in
+    let {
+      $dCategory_aLR :: Control.Category.Category g_aFo
+      [LclId]
+      $dCategory_aLR =
+        GHC.HetMet.GArrow.$p1GArrow
+          @ g_aFo
+          @ (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+          @ (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+          $dGArrow_aLQ } in
+    let {
+      $dGArrow_aMh
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrow_aMh =
+        $dGArrow_aLQ
+        `cast` (GHC.HetMet.GArrow.T:GArrow
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7
+                :: GHC.HetMet.GArrow.T:GArrow
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrow_aMi
+        :: GHC.HetMet.GArrow.GArrow
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrow_aMi =
+        $dGArrow_aMh
+        `cast` (GHC.HetMet.GArrow.T:GArrow g_aFo co_aM8 ()
+                :: GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+                     ~
+                   GHC.HetMet.GArrow.T:GArrow
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      $dGArrowDrop_aMf
+        :: GHC.HetMet.GArrow.GArrowDrop
+             g_aFo
+             (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+             (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+      [LclId]
+      $dGArrowDrop_aMf =
+        $dGArrowDrop_aLJ
+        `cast` (GHC.HetMet.GArrow.T:GArrowDrop
+                  g_aFo co_aM8 (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                :: GHC.HetMet.GArrow.T:GArrowDrop
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrowDrop
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)) } in
+    let {
+      $dGArrowDrop_aMg
+        :: GHC.HetMet.GArrow.GArrowDrop
+             g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()
+      [LclId]
+      $dGArrowDrop_aMg =
+        $dGArrowDrop_aMf
+        `cast` (GHC.HetMet.GArrow.T:GArrowDrop
+                  g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aM7
+                :: GHC.HetMet.GArrow.T:GArrowDrop
+                     g_aFo
+                     (GHC.HetMet.GArrow.GArrowTensor g_aFo)
+                     (GHC.HetMet.GArrow.GArrowUnit g_aFo)
+                     ~
+                   GHC.HetMet.GArrow.T:GArrowDrop
+                     g_aFo (GHC.HetMet.GArrow.GArrowTensor g_aFo) ()) } in
+    let {
+      @ co_aF3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aF3 = TYPE co_aFr } in
+    let {
+      @ co_aEX::() ~ ()
+      co_aEX = TYPE () } in
+    let {
+      @ co_aEI::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEI = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aEG::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEG = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aEF::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEF = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aEE::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aEE =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aF3)
+               (sym co_aEX) } in
+    let {
+      @ co_aEz::() ~ ()
+      co_aEz = TYPE () } in
+    let {
+      @ co_aF0::() ~ ()
+      co_aF0 = TYPE trans co_aEz co_aEX } in
+    let {
+      @ co_aEy::() ~ ()
+      co_aEy = TYPE () } in
+    let {
+      @ co_aEx::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEx =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEI)
+               (sym co_aEG) } in
+    let {
+      @ co_aEw::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEw = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aEH::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEH = TYPE trans co_aEw co_aEG } in
+    let {
+      @ co_aEv::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEv = TYPE GHC.HetMet.GArrow.GArrowTensor g_aFo } in
+    let {
+      @ co_aEu::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aEu =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEE)
+               (sym co_aEz) } in
+    let {
+      @ co_aEq::() ~ ()
+      co_aEq = TYPE () } in
+    let {
+      @ co_aEC::() ~ ()
+      co_aEC = TYPE trans co_aEq co_aEz } in
+    let {
+      @ co_aEZ::() ~ ()
+      co_aEZ = TYPE trans co_aEC co_aEX } in
+    let {
+      @ co_aEp::() ~ ()
+      co_aEp = TYPE () } in
+    let {
+      @ co_aEo::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aEo =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEu)
+               (sym co_aEq) } in
+    let {
+      @ co_aEl::() ~ ()
+      co_aEl = TYPE () } in
+    let {
+      @ co_aEs::() ~ ()
+      co_aEs = TYPE trans co_aEl co_aEq } in
+    let {
+      @ co_aED::() ~ ()
+      co_aED = TYPE trans co_aEs co_aEz } in
+    let {
+      @ co_aF1::() ~ ()
+      co_aF1 = TYPE trans co_aED co_aEX } in
+    let {
+      @ co_aEk::() ~ ()
+      co_aEk = TYPE () } in
+    let {
+      @ co_aEj::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aEj =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEo)
+               (sym co_aEl) } in
+    let {
+      @ co_aEh::() ~ ()
+      co_aEh = TYPE () } in
+    let {
+      @ co_aEn::() ~ ()
+      co_aEn = TYPE trans co_aEh co_aEl } in
+    let {
+      @ co_aEr::() ~ ()
+      co_aEr = TYPE trans co_aEn co_aEq } in
+    let {
+      @ co_aEA::() ~ ()
+      co_aEA = TYPE trans co_aEr co_aEz } in
+    let {
+      @ co_aEY::() ~ ()
+      co_aEY = TYPE trans co_aEA co_aEX } in
+    let {
+      @ co_aEg::() ~ ()
+      co_aEg = TYPE () } in
+    let {
+      @ co_aEf::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aEf = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in
+    let {
+      @ co_aEi::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aEi =
+        TYPE trans
+               co_aEf (GHC.HetMet.Private.PGArrow g_aFo co_aEh y_aFp) } in
+    let {
+      @ co_aEm::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aEm =
+        TYPE trans
+               co_aEi (GHC.HetMet.Private.PGArrow g_aFo co_aEl y_aFp) } in
+    let {
+      @ co_aEt::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aEt =
+        TYPE trans
+               co_aEm (GHC.HetMet.Private.PGArrow g_aFo co_aEq y_aFp) } in
+    let {
+      @ co_aEB::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aEB =
+        TYPE trans
+               co_aEt (GHC.HetMet.Private.PGArrow g_aFo co_aEz y_aFp) } in
+    let {
+      @ co_aF2::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aF2 =
+        TYPE trans
+               co_aEB (GHC.HetMet.Private.PGArrow g_aFo co_aEX y_aFp) } in
+    let {
+      @ co_aEd::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aEd = TYPE trans co_aEj (sym co_aEk) } in
+    let {
+      @ co_aEb::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aEb =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowTensor g_aFo) co_aEx)
+               (sym co_aEw) } in
+    let {
+      @ co_aE8::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aE8 = TYPE trans co_aEo (sym co_aEp) } in
+    let {
+      @ co_aE6::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aE6 = TYPE trans co_aEb (sym co_aEv) } in
+    let {
+      @ co_aE3::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aE3 = TYPE trans co_aEu (sym co_aEy) } in
+    let {
+      @ co_aE1::GHC.HetMet.GArrow.GArrowTensor g_aFo
+                  ~
+                GHC.HetMet.GArrow.GArrowTensor g_aFo
+      co_aE1 = TYPE trans co_aEx (sym co_aEF) } in
+    let {
+      @ co_aDD::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aDD = TYPE GHC.HetMet.Private.PGArrow g_aFo () y_aFp } in
+    let {
+      @ co_aDC::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aDC =
+        TYPE trans
+               (trans (GHC.HetMet.GArrow.GArrowUnit g_aFo) co_aEj)
+               (sym co_aEh) } in
+    let {
+      @ co_aDA::GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow
+                  g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
+      co_aDA =
+        TYPE trans
+               co_aDD
+               (GHC.HetMet.Private.PGArrow
+                  g_aFo
+                  (trans (sym co_aDC) (GHC.HetMet.GArrow.GArrowUnit g_aFo))
+                  y_aFp) } in
+    let {
+      @ co_aDv::GHC.HetMet.Private.PGArrow
+                  g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
+                  ~
+                GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+      co_aDv = TYPE sym co_aDA } in
+    let {
+      @ co_aDr::GHC.HetMet.GArrow.GArrowUnit g_aFo ~ ()
+      co_aDr = TYPE trans co_aDC (sym co_aEg) } in
+    let {
+      $dGArrowSTKC_aDm :: GHC.HetMet.GArrow.GArrowSTKC g_aFo
+      [LclId]
+      $dGArrowSTKC_aDm = $dGArrowSTKC_aFq } in
+    letrec {
+      foo'_aDw
+        :: GHC.HetMet.Private.PGArrow g_aFo () y_aFp -> g_aFo () y_aFp
+      [LclId]
+      foo'_aDw =
+        GHC.Base..
+          @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
+          @ (g_aFo () y_aFp)
+          @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
+          (GHC.HetMet.Private.unG @ g_aFo @ () @ y_aFp $dGArrowSTKC_aDm)
+          (GHC.Base..
+             @ <[y_aFp]>@g_aFo
+             @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
+             @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
+             ((GHC.HetMet.CodeTypes.pga_flatten @ g_aFo @ GHC.Prim.Any @ y_aFp)
+              `cast` (<[y_aFp]>@g_aFo
+                      -> GHC.HetMet.Private.PGArrow g_aFo co_aDr y_aFp
+                      :: (<[y_aFp]>@g_aFo
+                          -> GHC.HetMet.Private.PGArrow
+                               g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp)
+                           ~
+                         (<[y_aFp]>@g_aFo -> GHC.HetMet.Private.PGArrow g_aFo () y_aFp)))
+             (GHC.Base..
+                @ <[y_aFp]>@g_aFo
+                @ <[y_aFp]>@g_aFo
+                @ (GHC.HetMet.Private.PGArrow g_aFo () y_aFp)
+                (Main.foo @ g_aFo @ y_aFp)
+                ((GHC.HetMet.CodeTypes.pga_unflatten
+                    @ g_aFo @ GHC.Prim.Any @ y_aFp)
+                 `cast` (co_aDv -> <[y_aFp]>@g_aFo
+                         :: (GHC.HetMet.Private.PGArrow
+                               g_aFo (GHC.HetMet.GArrow.GArrowUnit g_aFo) y_aFp
+                             -> <[y_aFp]>@g_aFo)
+                              ~
+                            (GHC.HetMet.Private.PGArrow g_aFo () y_aFp
+                             -> <[y_aFp]>@g_aFo))))); } in
+    foo'_aDw
+
+Main.main :: GHC.Types.IO ()
+[LclIdX]
+Main.main =
+  let {
+    @ co_aLu::GHC.Types.Int ~ GHC.Types.Int
+    co_aLu = TYPE GHC.Types.Int } in
+  let {
+    @ co_aLt::GHC.Types.Int ~ GHC.Types.Int
+    co_aLt = TYPE GHC.Types.Int } in
+  letrec {
+    main_aHj :: GHC.Types.IO ()
+    [LclId]
+    main_aHj =
+      GArrowTikZ.tikz
+        @ ()
+        @ GHC.Types.Int
+        (Main.foo'
+           @ GArrowTikZ.GArrowTikZ
+           @ GHC.Types.Int
+           $dGArrowSTKC_aHd
+           @ co_aHe
+           (GHC.HetMet.Private.PGArrowD
+              @ GArrowTikZ.GArrowTikZ
+              @ ()
+              @ GHC.Types.Int
+              (\ ($dGArrowSTKC_aHg
+                    :: GHC.HetMet.GArrow.GArrowSTKC GArrowTikZ.GArrowTikZ) ->
+                 let {
+                   @ co_aHD::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                   co_aHD =
+                     TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aHG::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
+                   co_aHG =
+                     TYPE trans (sym co_aHD) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
+                 let {
+                   @ co_aHB::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                   co_aHB =
+                     TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aHH::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             (,)
+                   co_aHH =
+                     TYPE trans
+                            (sym co_aHB) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
+                 let {
+                   @ co_aHx::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                   co_aHx =
+                     TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aLd::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
+                   co_aLd =
+                     TYPE trans (sym co_aHx) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
+                 let {
+                   @ co_aHv::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                   co_aHv =
+                     TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aLe::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             (,)
+                   co_aLe =
+                     TYPE trans
+                            (sym co_aHv) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
+                 let {
+                   @ co_aHr::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ
+                   co_aHr =
+                     TYPE GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aLf::GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ ~ ()
+                   co_aLf =
+                     TYPE trans (sym co_aHr) GArrowTikZ.TFCo:R:GArrowUnitGArrowTikZ } in
+                 let {
+                   @ co_aHp::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                   co_aHp =
+                     TYPE GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ } in
+                 let {
+                   @ co_aLg::GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ
+                               ~
+                             (,)
+                   co_aLg =
+                     TYPE trans
+                            (sym co_aHp) GArrowTikZ.TFCo:R:GArrowTensorGArrowTikZ } in
+                 let {
+                   $dGArrowSwap_aHn
+                     :: GHC.HetMet.GArrow.GArrowSwap
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrowSwap_aHn =
+                     GHC.HetMet.GArrow.$p3GArrowSTKC
+                       @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
+                 let {
+                   $dGArrow_aHE
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrow_aHE =
+                     GHC.HetMet.GArrow.$p1GArrowSwap
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrowSwap_aHn } in
+                 let {
+                   $dCategory_aHF :: Control.Category.Category GArrowTikZ.GArrowTikZ
+                   [LclId]
+                   $dCategory_aHF =
+                     GHC.HetMet.GArrow.$p1GArrow
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrow_aHE } in
+                 let {
+                   $dGArrow_aLj
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (,)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrow_aLj =
+                     $dGArrow_aHE
+                     `cast` (GHC.HetMet.GArrow.T:GArrow
+                               GArrowTikZ.GArrowTikZ
+                               co_aHH
+                               (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
+                 let {
+                   $dGArrow_aLk
+                     :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrow_aLk =
+                     $dGArrow_aLj
+                     `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) co_aHG
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   $dGArrowSwap_aLh
+                     :: GHC.HetMet.GArrow.GArrowSwap
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          ()
+                   [LclId]
+                   $dGArrowSwap_aLh =
+                     $dGArrowSwap_aHn
+                     `cast` (GHC.HetMet.GArrow.T:GArrowSwap
+                               GArrowTikZ.GArrowTikZ
+                               (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                               co_aHG
+                             :: GHC.HetMet.GArrow.T:GArrowSwap
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowSwap
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()) } in
+                 let {
+                   $dGArrowSwap_aLi
+                     :: GHC.HetMet.GArrow.GArrowSwap GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrowSwap_aLi =
+                     $dGArrowSwap_aLh
+                     `cast` (GHC.HetMet.GArrow.T:GArrowSwap
+                               GArrowTikZ.GArrowTikZ co_aHH ()
+                             :: GHC.HetMet.GArrow.T:GArrowSwap
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowSwap GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   $dGArrowCopy_aHm
+                     :: GHC.HetMet.GArrow.GArrowCopy
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrowCopy_aHm =
+                     GHC.HetMet.GArrow.$p2GArrowSTKC
+                       @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
+                 let {
+                   $dGArrow_aHy
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrow_aHy =
+                     GHC.HetMet.GArrow.$p1GArrowCopy
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrowCopy_aHm } in
+                 let {
+                   $dCategory_aHz :: Control.Category.Category GArrowTikZ.GArrowTikZ
+                   [LclId]
+                   $dCategory_aHz =
+                     GHC.HetMet.GArrow.$p1GArrow
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrow_aHy } in
+                 let {
+                   $dGArrow_aLn
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          ()
+                   [LclId]
+                   $dGArrow_aLn =
+                     $dGArrow_aHy
+                     `cast` (GHC.HetMet.GArrow.T:GArrow
+                               GArrowTikZ.GArrowTikZ
+                               (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                               co_aLd
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()) } in
+                 let {
+                   $dGArrow_aLo
+                     :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrow_aLo =
+                     $dGArrow_aLn
+                     `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLe ()
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   $dGArrowCopy_aLl
+                     :: GHC.HetMet.GArrow.GArrowCopy
+                          GArrowTikZ.GArrowTikZ
+                          (,)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrowCopy_aLl =
+                     $dGArrowCopy_aHm
+                     `cast` (GHC.HetMet.GArrow.T:GArrowCopy
+                               GArrowTikZ.GArrowTikZ
+                               co_aLe
+                               (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                             :: GHC.HetMet.GArrow.T:GArrowCopy
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowCopy
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
+                 let {
+                   $dGArrowCopy_aLm
+                     :: GHC.HetMet.GArrow.GArrowCopy GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrowCopy_aLm =
+                     $dGArrowCopy_aLl
+                     `cast` (GHC.HetMet.GArrow.T:GArrowCopy
+                               GArrowTikZ.GArrowTikZ (,) co_aLd
+                             :: GHC.HetMet.GArrow.T:GArrowCopy
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowCopy GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   $dGArrowDrop_aHl
+                     :: GHC.HetMet.GArrow.GArrowDrop
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrowDrop_aHl =
+                     GHC.HetMet.GArrow.$p1GArrowSTKC
+                       @ GArrowTikZ.GArrowTikZ $dGArrowSTKC_aHg } in
+                 let {
+                   $dGArrow_aHs
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrow_aHs =
+                     GHC.HetMet.GArrow.$p1GArrowDrop
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrowDrop_aHl } in
+                 let {
+                   $dCategory_aHt :: Control.Category.Category GArrowTikZ.GArrowTikZ
+                   [LclId]
+                   $dCategory_aHt =
+                     GHC.HetMet.GArrow.$p1GArrow
+                       @ GArrowTikZ.GArrowTikZ
+                       @ (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                       @ (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                       $dGArrow_aHs } in
+                 let {
+                   $dGArrow_aLr
+                     :: GHC.HetMet.GArrow.GArrow
+                          GArrowTikZ.GArrowTikZ
+                          (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                          ()
+                   [LclId]
+                   $dGArrow_aLr =
+                     $dGArrow_aHs
+                     `cast` (GHC.HetMet.GArrow.T:GArrow
+                               GArrowTikZ.GArrowTikZ
+                               (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                               co_aLf
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()) } in
+                 let {
+                   $dGArrow_aLs
+                     :: GHC.HetMet.GArrow.GArrow GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrow_aLs =
+                     $dGArrow_aLr
+                     `cast` (GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ co_aLg ()
+                             :: GHC.HetMet.GArrow.T:GArrow
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  ()
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrow GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   $dGArrowDrop_aLp
+                     :: GHC.HetMet.GArrow.GArrowDrop
+                          GArrowTikZ.GArrowTikZ
+                          (,)
+                          (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                   [LclId]
+                   $dGArrowDrop_aLp =
+                     $dGArrowDrop_aHl
+                     `cast` (GHC.HetMet.GArrow.T:GArrowDrop
+                               GArrowTikZ.GArrowTikZ
+                               co_aLg
+                               (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                             :: GHC.HetMet.GArrow.T:GArrowDrop
+                                  GArrowTikZ.GArrowTikZ
+                                  (GHC.HetMet.GArrow.GArrowTensor GArrowTikZ.GArrowTikZ)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowDrop
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)) } in
+                 let {
+                   $dGArrowDrop_aLq
+                     :: GHC.HetMet.GArrow.GArrowDrop GArrowTikZ.GArrowTikZ (,) ()
+                   [LclId]
+                   $dGArrowDrop_aLq =
+                     $dGArrowDrop_aLp
+                     `cast` (GHC.HetMet.GArrow.T:GArrowDrop
+                               GArrowTikZ.GArrowTikZ (,) co_aLf
+                             :: GHC.HetMet.GArrow.T:GArrowDrop
+                                  GArrowTikZ.GArrowTikZ
+                                  (,)
+                                  (GHC.HetMet.GArrow.GArrowUnit GArrowTikZ.GArrowTikZ)
+                                  ~
+                                GHC.HetMet.GArrow.T:GArrowDrop GArrowTikZ.GArrowTikZ (,) ()) } in
+                 let {
+                   @ co_aHh::GHC.Types.Int ~ GHC.Types.Int
+                   co_aHh = TYPE sym co_aLt } in
+                 (GArrowTikZ.$WTikZ_const (GHC.Types.I# 12))
+                 `cast` (GArrowTikZ.GArrowTikZ () co_aHh
+                         :: GArrowTikZ.GArrowTikZ () GHC.Types.Int
+                              ~
+                            GArrowTikZ.GArrowTikZ () GHC.Types.Int)))); } in
+  main_aHj
+
+:Main.main :: GHC.Types.IO ()
+[LclIdX]
+:Main.main = GHC.TopHandler.runMainIO @ () Main.main
+end Rec }
+
+
+
+
+==================== Desugar ====================
+Main.foo
+  :: forall (tv_~N6 :: * -> * -> *) tv_~N7.
+     GHC.HetMet.Private.PGArrow
+       tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
+     -> GHC.HetMet.Private.PGArrow
+          tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
+[LclId]
+Main.foo =
+  \ (@ tv_~N6::* -> * -> *)
+    (@ tv_~N7)
+    (ev_~N8
+       :: GHC.HetMet.Private.PGArrow
+            tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7) ->
+    let {
+      ev_~N9
+        :: GHC.HetMet.Private.PGArrow
+             tv_~N6
+             (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+             (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+      [LclId]
+      ev_~N9 =
+        GHC.HetMet.Private.pga_id
+          @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
+    let {
+      ev_~Na
+        :: GHC.HetMet.Private.PGArrow
+             tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
+      [LclId]
+      ev_~Na =
+        let {
+          ev_~Nh
+            :: GHC.HetMet.Private.PGArrow
+                 tv_~N6
+                 (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+                 (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+          [LclId]
+          ev_~Nh =
+            GHC.HetMet.Private.pga_id
+              @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
+        let {
+          ev_~Ni
+            :: GHC.HetMet.Private.PGArrow
+                 tv_~N6 (GHC.HetMet.GArrow.GArrowUnit tv_~N6) tv_~N7
+          [LclId]
+          ev_~Ni = ev_~N8 } in
+        let {
+          ev_~Nj
+            :: GHC.HetMet.Private.PGArrow
+                 tv_~N6
+                 (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+                 (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+          [LclId]
+          ev_~Nj =
+            GHC.HetMet.Private.pga_drop
+              @ tv_~N6 @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6) } in
+        GHC.HetMet.Private.pga_comp
+          @ tv_~N6
+          @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+          @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+          @ tv_~N7
+          ev_~Nj
+          ev_~Ni } in
+    GHC.HetMet.Private.pga_comp
+      @ tv_~N6
+      @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+      @ (GHC.HetMet.GArrow.GArrowUnit tv_~N6)
+      @ tv_~N7
+      ev_~N9
+      ev_~Na
+
+Main.maincoercionKind
+    base:GHC.HetMet.GArrow.GArrowUnit{tc 02y}
+      main:GArrowTikZ.GArrowTikZ{tc roV}
+      ~
+    ghc-prim:GHC.Unit.(){(w) tc 40}
+ghc-stage2: coreTypeToWeakType
+  hit a bare EqPred

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 7e68ba0..0775229 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -53,8 +53,10 @@ sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT e
 coreVarToWeakVar :: Var.Var -> WeakVar
 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
-coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") 
-                                                             (Prelude.error "FIXME") (Prelude.error "FIXME"))
+coreVarToWeakVar v | Var.isCoVar v
+  = WCoerVar (WeakCoerVar v
+                          (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v)))))
+                          (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v))))))
 coreVarToWeakVar _                 =
    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
 
@@ -87,8 +89,9 @@ sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
 kindToCoreKind :: Kind -> TypeRep.Kind
 kindToCoreKind KindStar          = TypeRep.liftedTypeKind
 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
-kindToCoreKind _                 = Prelude.error "kindToCoreKind does not know how to handle that"
-
+kindToCoreKind k                 = Prelude.error ((Prelude.++)
+                                                    "kindToCoreKind does not know how to handle kind "
+                                                                               (kindToString k))
 coreKindToKind :: TypeRep.Kind -> Kind
 coreKindToKind k =
   case Coercion.splitKindFunTy_maybe k of

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index cae7174..3cd8ff6 100644 (file)
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -161,7 +161,7 @@ Section core2proof.
     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
-      weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
+      weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 
@@ -280,6 +280,9 @@ Section core2proof.
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_PGArrow_unit_TyCon : TyFun)
+    (hetmet_PGArrow_tensor_TyCon : TyFun)
+    (hetmet_PGArrow_exponent_TyCon : TyFun)
     (hetmet_pga_id : CoreVar)
     (hetmet_pga_comp : CoreVar)
     (hetmet_pga_first : CoreVar)
@@ -299,9 +302,11 @@ Section core2proof.
     (hetmet_pga_curryr : CoreVar)
     .
 
-    Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
-    Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
-      TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
+
+    Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
+      @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+    Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
+      TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b.
     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
       TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
@@ -370,22 +375,22 @@ Section core2proof.
           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
       Defined.
 
-    Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
+    Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ ec x.
 
     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
-    { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
-    ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
-    ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
-    ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
-    ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
-    ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
-    ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
-    ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
-    ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
-    ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
-    ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
-    ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
-    ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
+    { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat ec a)
+    ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat ec a)
+    ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat ec a)
+    ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
+    ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
+    ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+    ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+    ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b)
+    ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat ec a)
+    ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat ec a)
+    ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec x))
+    ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
@@ -464,6 +469,9 @@ Section core2proof.
     (uniqueSupply : UniqSupply)
     (lbinds:list (@CoreBind CoreVar))
     (hetmet_PGArrowTyCon : TyFun)
+    (hetmet_PGArrow_unit_TyCon : TyFun)
+    (hetmet_PGArrow_tensor_TyCon : TyFun)
+    (hetmet_PGArrow_exponent_TyCon : TyFun)
     (hetmet_pga_id : CoreVar)
     (hetmet_pga_comp : CoreVar)
     (hetmet_pga_first : CoreVar)
@@ -489,6 +497,9 @@ Section core2proof.
        hetmet_flattened_id
        uniqueSupply 
        hetmet_PGArrowTyCon
+       hetmet_PGArrow_unit_TyCon
+       hetmet_PGArrow_tensor_TyCon
+(*       hetmet_PGArrow_exponent_TyCon*)
        hetmet_pga_id 
        hetmet_pga_comp 
        hetmet_pga_first 

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index ac2da8c..78223cf 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -69,9 +69,11 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                 coreTypeToWeakType' t2 >>= fun t2' => 
                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
   | ForAllTy cv t            => match coreVarToWeakVar cv with
-                                  | WExprVar _  => Error "encountered expression variable in a type"
+                                  | WExprVar _  => Error "encountered expression variable in a type abstraction"
                                   | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
-                                  | WCoerVar _  => Error "encountered coercion variable in a type"
+                                  | WCoerVar (weakCoerVar v t1' t2') => 
+                                        coreTypeToWeakType' t >>= fun t3' => 
+                                          OK (WCoFunTy t1' t2' t3')
                                 end
   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with 
                                                   | nil => OK nil
@@ -82,7 +84,8 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 
-Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
+Definition coreTypeToWeakType t :=
+  addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 677287a..4babf36 100644 (file)
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -36,7 +36,8 @@ Extract Inductive PredType =>
 
 Variable coreNameToString      : CoreName     -> string.    Extract Inlined Constant coreNameToString       => "outputableToString".
 Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Constant coreCoercionToString   => "outputableToString".
-Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
+Variable coreCoercionKind : Kind -> CoreType*CoreType.
+  Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
 Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index b46f4d2..a23acfd 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -97,15 +97,15 @@ Section HaskFlattener.
   Context (hetmet_flatten : WeakExprVar).
   Context (hetmet_unflatten : WeakExprVar).
   Context (hetmet_id      : WeakExprVar).
-  Context {unitTy : forall TV, RawHaskType TV ★                                          }.
-  Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
+  Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
+  Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 
-  Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
-    fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
+  Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
+    fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (mapOptionTree (fun x => x TV ite) tr).
 
   Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
-    fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
+    fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 
   Class garrow :=
   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a a @@ l] ]
@@ -148,7 +148,7 @@ Section HaskFlattener.
     | TCoerc _ t1 t2 t      => TCoerc    (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
                                          (garrowfy_raw_codetypes t)
     | TArrow                => TArrow
-    | TCode      v e        => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
+    | TCode      v e        => gaTy TV v (unitTy TV v) (garrowfy_raw_codetypes e)
     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
     end
     with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index f5a3f1a..8ceb0b7 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -72,7 +72,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
-  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
+  | WECoLam (weakCoerVar cv   _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
                                                    ((CoreEType (TyVarTy ec))::

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 0055a17..d77d074 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -19,6 +19,7 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -416,7 +417,7 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex
   Defined.
 
 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
-  match wcv with weakCoerVar _ κ _ _ => κ end.
+  match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 
 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
@@ -631,7 +632,7 @@ Definition weakExprToStrongExpr : forall
                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
                                            end
 
-    | WECoLam cv e                      => let (_,_,t1,t2) := cv in
+    | WECoLam cv e                      => let (_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 9b34188..9ec126e 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -47,7 +47,7 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
     Defined.
 
 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
-Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
 
 Inductive WeakCoercion : Type :=
 | WCoVar          : WeakCoerVar                                   -> WeakCoercion (* g      *)
@@ -66,7 +66,7 @@ Inductive WeakCoercion : Type :=
 
 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
 match wc with
-| WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
+| WCoVar     (weakCoerVar _ t1 t2)   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoType    t                       => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoApp     c1 c2                   => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)
 | WCoAppT    c t                     => (WFunTyCon,WFunTyCon)   (* FIXME!!! *)

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index 8cb9da6..896aff4 100644 (file)
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -32,9 +32,9 @@ Definition weakTypeVarToKind (tv:WeakTypeVar) : Kind :=
 
 Definition weakVarToCoreVar (wv:WeakVar) : CoreVar :=
   match wv with
-  | WExprVar (weakExprVar v _    ) => v
-  | WTypeVar (weakTypeVar v _    ) => v
-  | WCoerVar (weakCoerVar v _ _ _) => v
+  | WExprVar (weakExprVar v _  ) => v
+  | WTypeVar (weakTypeVar v _  ) => v
+  | WCoerVar (weakCoerVar v _ _) => v
  end.
  Coercion weakVarToCoreVar : WeakVar >-> CoreVar.