autoWeak: Improve typing

- Check that source layout is actually a subset of the target layout
  statically, because we can and it prevents runtime errors (I didn't
  actually get such an error yet, but I worried about it too much)
- Use less Append in type of (&.) to make type errors _significantly_
  less verbose

1 files changed, 30 insertions, 14 deletions

diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs
index c6efe37..7370df1 100644
--- a/src/AST/Weaken/Auto.hs
+++ b/src/AST/Weaken/Auto.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {-# LANGUAGE AllowAmbiguousTypes #-}
 
@@ -23,6 +24,7 @@ module AST.Weaken.Auto (
 ) where
 
 import Data.Functor.Const
+import Data.Kind (Constraint)
 import GHC.OverloadedLabels
 import GHC.TypeLits
 import Unsafe.Coerce (unsafeCoerce)
@@ -39,18 +41,21 @@ type family Lookup name list where
 
 
 -- | The @withPre@ type parameter indicates whether there can be 'LPreW'
--- occurrences within this layout.
-data Layout (withPre :: Bool) (segments :: [(Symbol, [t])]) (env :: [t]) where
-  LSeg :: forall name segments withPre. SSymbol name -> Layout withPre segments (Lookup name segments)
+-- occurrences within this layout. 'names' is the list of names that this
+-- layout /produces/. That is: for LPreW, it contains the target name. The
+-- 'names' list of a source layout must be a subset of the names list of the
+-- target layout (which cannot contain LPreW); this is checked with SubLayout.
+data Layout (withPre :: Bool) (segments :: [(Symbol, [t])]) (names :: [Symbol]) (env :: [t]) where
+  LSeg :: forall name segments withPre. SSymbol name -> Layout withPre segments '[name] (Lookup name segments)
   -- | Pre-weaken with a weakening
   LPreW :: forall name1 name2 segments.
            SegmentName name1 -> SegmentName name2
         -> Lookup name1 segments :> Lookup name2 segments
-        -> Layout True segments (Lookup name1 segments)
-  (:++:) :: Layout withPre segments env1 -> Layout withPre segments env2 -> Layout withPre segments (Append env1 env2)
+        -> Layout True segments '[name2] (Lookup name1 segments)
+  (:++:) :: Layout withPre segments names1 env1 -> Layout withPre segments names2 env2 -> Layout withPre segments (Append names1 names2) (Append env1 env2)
 infixr :++:
 
-instance (KnownSymbol name, seg ~ Lookup name segments) => IsLabel name (Layout withPre segments seg) where
+instance (KnownSymbol name, seg ~ Lookup name segments, names ~ '[name]) => IsLabel name (Layout withPre segments names seg) where
   fromLabel = LSeg (symbolSing @name)
 
 newtype SegmentName name = SegmentName (SSymbol name)
@@ -60,6 +65,18 @@ instance (KnownSymbol name, name ~ name') => IsLabel name (SegmentName name') wh
   fromLabel = SegmentName symbolSing
 
 
+type family SubLayout names1 names2 where
+  SubLayout '[] _ = () :: Constraint
+  SubLayout (n : names1) names2 = SubLayout' n (Contains n names2) names1 names2
+type family SubLayout' n ok names1 names2 where
+  SubLayout' n False _ _ = TypeError (Text "The name '" :<>: Text n :<>: Text "' appears in the source layout but not in the target.")
+  SubLayout' _ True names1 names2 = SubLayout names1 names2
+type family Contains n names where
+  Contains _ '[] = False
+  Contains n (n : _) = True
+  Contains n (_ : names) = Contains n names
+
+
 data SSegments (segments :: [(Symbol, [t])]) where
   SSegNil :: SSegments '[]
   SSegCons :: SSymbol name -> SList (Const ()) ts -> SSegments list -> SSegments ('(name, ts) : list)
@@ -74,7 +91,7 @@ auto1 :: SList (Const ()) '[t]
 auto1 = Const () `SCons` SNil
 
 infixr &.
-(&.) :: SSegments segs1 -> SSegments segs2 -> SSegments (Append segs1 segs2)
+(&.) :: SSegments '[segs1] -> SSegments segs2 -> SSegments (segs1 : segs2)
 (&.) = ssegmentsAppend
   where
     ssegmentsAppend :: SSegments a -> SSegments b -> SSegments (Append a b)
@@ -118,12 +135,12 @@ linLayoutAppend (LinAppPreW (name1 :: SSymbol name1) name2 w (lin1 :: LinLayout
   | Refl <- lemAppendAssoc @(Lookup name1 segments) @env1' @env2
   = LinAppPreW name1 name2 w (linLayoutAppend lin1 lin2)
 
-lineariseLayout :: Layout withPre segments env -> LinLayout withPre segments env
-lineariseLayout (LSeg name :: Layout _ _ seg)
+lineariseLayout :: Layout withPre segments names env -> LinLayout withPre segments env
+lineariseLayout (LSeg name :: Layout _ _ _ seg)
   | Refl <- lemAppendNil @seg
   = LinApp name LinEnd
 lineariseLayout (ly1 :++: ly2) = lineariseLayout ly1 `linLayoutAppend` lineariseLayout ly2
-lineariseLayout (LPreW (SegmentName name1) (SegmentName name2) w :: Layout _ _ seg)
+lineariseLayout (LPreW (SegmentName name1) (SegmentName name2) w :: Layout _ _ _ seg)
   | Refl <- lemAppendNil @seg
   = LinAppPreW name1 name2 w LinEnd
 
@@ -151,8 +168,7 @@ pullDown segs name@SSymbol linlayout kNotFound k =
             k (LinApp n' lin') (WSwap @env' (segmentLookup segs n') (segmentLookup segs name)
                                   .> wCopies (segmentLookup segs n') w)
 
-sortLinLayouts :: forall segments env1 env2.
-                  SSegments segments
+sortLinLayouts :: SSegments segments
                -> LinLayout False segments env1 -> LinLayout False segments env2 -> env1 :> env2
 sortLinLayouts _ LinEnd LinEnd = WId
 sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail2)
@@ -169,8 +185,8 @@ sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail
 sortLinLayouts _ LinEnd LinApp{} = WClosed
 sortLinLayouts _ LinApp{} LinEnd = error "Segments in source that do not occur in target"
 
-autoWeak :: forall segments env1 env2.
-            SSegments segments -> Layout True segments env1 -> Layout False segments env2 -> env1 :> env2
+autoWeak :: SubLayout names1 names2
+         => SSegments segments -> Layout True segments names1 env1 -> Layout False segments names2 env2 -> env1 :> env2
 autoWeak segs ly1 ly2 =
   preWeaken segs (lineariseLayout ly1) $ \wPreweak lin1 ->
     sortLinLayouts segs lin1 (lineariseLayout ly2) .> wPreweak