Compilation failure when unsafe-operations is disabled

[RyanGlScott]

If you build parameterized-utils with the unsafe-operations flag disabled, it will fail to compile:

$ cabal build -f-unsafe-operations
Build profile: -w ghc-8.10.4 -O1
In order, the following will be built (use -v for more details):
 - parameterized-utils-2.1.3.0.100 (lib) (file src/Data/Parameterized/Peano.hs changed)
Preprocessing library for parameterized-utils-2.1.3.0.100..
Building library for parameterized-utils-2.1.3.0.100..
[31 of 32] Compiling Data.Parameterized.Peano

src/Data/Parameterized/Peano.hs:326:1: error: [-Wincomplete-patterns, -Werror=incomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘plusP’:
        Patterns not matched:
            ZRepr ZRepr
            ZRepr (SRepr _)
    |
326 | plusP (SRepr a) b = SRepr (plusP a b)
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

That particular error is easy enough to fix:

diff --git a/src/Data/Parameterized/Peano.hs b/src/Data/Parameterized/Peano.hs
index 55c97ca..7a5a5e6 100644
--- a/src/Data/Parameterized/Peano.hs
+++ b/src/Data/Parameterized/Peano.hs
@@ -323,6 +323,7 @@ plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
 #ifdef UNSAFE_OPS
 plusP (PeanoRepr a) (PeanoRepr b) = PeanoRepr (a + b)
 #else
+plusP ZRepr     b = b
 plusP (SRepr a) b = SRepr (plusP a b)
 #endif

However, there are more errors waiting in the test suite:

$ cabal test -f-unsafe-operations
Build profile: -w ghc-8.10.4 -O1
In order, the following will be built (use -v for more details):
 - parameterized-utils-2.1.3.0.100 (test:parameterizedTests) (first run)
Preprocessing test suite 'parameterizedTests' for parameterized-utils-2.1.3.0.100..
Building test suite 'parameterizedTests' for parameterized-utils-2.1.3.0.100..
[1 of 7] Compiling Test.Context

test/Test/Context.hs:241:34: error:
    • Couldn't match expected type ‘S.Size b0’
                  with actual type ‘U.Size 'EmptyCtx’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.take’, namely ‘U.zeroSize’
      In the expression: C.take U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.take U.zeroSize (U.size z) z
    • Relevant bindings include
        r :: S.Assignment f0 b0 (bound at test/Test/Context.hs:241:23)
    |
241 |           Refl -> let r = C.take U.zeroSize (U.size z) z in
    |                                  ^^^^^^^^^^

test/Test/Context.hs:241:46: error:
    • Couldn't match expected type ‘S.Size ctx'0’
                  with actual type ‘U.Size (EmptyCtx <+> ((x <+> x1) <+> x2))’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.take’, namely ‘(U.size z)’
      In the expression: C.take U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.take U.zeroSize (U.size z) z
    • Relevant bindings include
        r :: S.Assignment f0 b0 (bound at test/Test/Context.hs:241:23)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:239:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:238:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:237:14)
        w :: UAsgn x (bound at test/Test/Context.hs:236:14)
    |
241 |           Refl -> let r = C.take U.zeroSize (U.size z) z in
    |                                              ^^^^^^^^

test/Test/Context.hs:241:56: error:
    • Couldn't match expected type ‘S.Assignment f0 (b0 <+> ctx'0)’
                  with actual type ‘U.Assignment Payload ((x <+> x1) <+> x2)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.take’, namely ‘z’
      In the expression: C.take U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.take U.zeroSize (U.size z) z
    • Relevant bindings include
        r :: S.Assignment f0 b0 (bound at test/Test/Context.hs:241:23)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:239:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:238:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:237:14)
        w :: UAsgn x (bound at test/Test/Context.hs:236:14)
    |
241 |           Refl -> let r = C.take U.zeroSize (U.size z) z in
    |                                                        ^

test/Test/Context.hs:242:60: error:
    • Couldn't match type ‘S.Assignment f0’
                     with ‘U.Assignment f1’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment f1 b0
        Actual type: S.Assignment f0 b0
    • In the second argument of ‘testEquality’, namely ‘r’
      In the second argument of ‘($)’, namely ‘testEquality U.empty r’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality U.empty r’
    • Relevant bindings include
        r :: S.Assignment f0 b0 (bound at test/Test/Context.hs:241:23)
    |
242 |                     assert $ isJust $ testEquality U.empty r
    |                                                            ^

test/Test/Context.hs:252:34: error:
    • Couldn't match expected type ‘S.Size ctx0’
                  with actual type ‘U.Size 'EmptyCtx’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.drop’, namely ‘U.zeroSize’
      In the expression: C.drop U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.drop U.zeroSize (U.size z) z
    |
252 |           Refl -> let r = C.drop U.zeroSize (U.size z) z in
    |                                  ^^^^^^^^^^

test/Test/Context.hs:252:46: error:
    • Couldn't match expected type ‘S.Size b1’
                  with actual type ‘U.Size (EmptyCtx <+> ((x <+> x1) <+> x2))’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.drop’, namely ‘(U.size z)’
      In the expression: C.drop U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.drop U.zeroSize (U.size z) z
    • Relevant bindings include
        r :: S.Assignment f2 b1 (bound at test/Test/Context.hs:252:23)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:250:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:249:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:248:14)
        w :: UAsgn x (bound at test/Test/Context.hs:247:14)
    |
252 |           Refl -> let r = C.drop U.zeroSize (U.size z) z in
    |                                              ^^^^^^^^

test/Test/Context.hs:252:56: error:
    • Couldn't match expected type ‘S.Assignment f2 (ctx0 <+> b1)’
                  with actual type ‘U.Assignment Payload ((x <+> x1) <+> x2)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.drop’, namely ‘z’
      In the expression: C.drop U.zeroSize (U.size z) z
      In an equation for ‘r’: r = C.drop U.zeroSize (U.size z) z
    • Relevant bindings include
        r :: S.Assignment f2 b1 (bound at test/Test/Context.hs:252:23)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:250:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:249:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:248:14)
        w :: UAsgn x (bound at test/Test/Context.hs:247:14)
    |
252 |           Refl -> let r = C.drop U.zeroSize (U.size z) z in
    |                                                        ^

test/Test/Context.hs:253:54: error:
    • Couldn't match type ‘S.Assignment f2’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b1
        Actual type: S.Assignment f2 b1
    • In the second argument of ‘testEquality’, namely ‘r’
      In the second argument of ‘($)’, namely ‘testEquality z r’
      In the second argument of ‘($)’, namely ‘isJust $ testEquality z r’
    • Relevant bindings include
        r :: S.Assignment f2 b1 (bound at test/Test/Context.hs:252:23)
    |
253 |                     assert $ isJust $ testEquality z r
    |                                                      ^

test/Test/Context.hs:263:25: error:
    • Couldn't match expected type ‘S.Size b2’
                  with actual type ‘U.Size ((x <+> x1) <+> x2)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.take’, namely ‘(U.size z)’
      In the expression: C.take (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.take (U.size z) U.zeroSize z
    • Relevant bindings include
        r :: S.Assignment f3 b2 (bound at test/Test/Context.hs:263:13)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:262:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:261:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:260:14)
        w :: UAsgn x (bound at test/Test/Context.hs:259:14)
    |
263 |         let r = C.take (U.size z) U.zeroSize z
    |                         ^^^^^^^^

test/Test/Context.hs:263:35: error:
    • Couldn't match expected type ‘S.Size ctx'1’
                  with actual type ‘U.Size 'EmptyCtx’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.take’, namely ‘U.zeroSize’
      In the expression: C.take (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.take (U.size z) U.zeroSize z
    |
263 |         let r = C.take (U.size z) U.zeroSize z
    |                                   ^^^^^^^^^^

test/Test/Context.hs:263:46: error:
    • Couldn't match expected type ‘S.Assignment f3 (b2 <+> ctx'1)’
                  with actual type ‘U.Assignment Payload ((x <+> x1) <+> x2)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.take’, namely ‘z’
      In the expression: C.take (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.take (U.size z) U.zeroSize z
    • Relevant bindings include
        r :: S.Assignment f3 b2 (bound at test/Test/Context.hs:263:13)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:262:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:261:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:260:14)
        w :: UAsgn x (bound at test/Test/Context.hs:259:14)
    |
263 |         let r = C.take (U.size z) U.zeroSize z
    |                                              ^

test/Test/Context.hs:264:42: error:
    • Couldn't match type ‘S.Assignment f3’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b2
        Actual type: S.Assignment f3 b2
    • In the second argument of ‘testEquality’, namely ‘r’
      In the second argument of ‘($)’, namely ‘testEquality z r’
      In the second argument of ‘($)’, namely ‘isJust $ testEquality z r’
    • Relevant bindings include
        r :: S.Assignment f3 b2 (bound at test/Test/Context.hs:263:13)
    |
264 |         assert $ isJust $ testEquality z r
    |                                          ^

test/Test/Context.hs:273:25: error:
    • Couldn't match expected type ‘S.Size ctx1’
                  with actual type ‘U.Size ((x <+> x1) <+> x2)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.drop’, namely ‘(U.size z)’
      In the expression: C.drop (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.drop (U.size z) U.zeroSize z
    • Relevant bindings include
        r :: S.Assignment f4 b3 (bound at test/Test/Context.hs:273:13)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:272:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:271:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:270:14)
        w :: UAsgn x (bound at test/Test/Context.hs:269:14)
    |
273 |         let r = C.drop (U.size z) U.zeroSize z
    |                         ^^^^^^^^

test/Test/Context.hs:273:35: error:
    • Couldn't match expected type ‘S.Size b3’
                  with actual type ‘U.Size 'EmptyCtx’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.drop’, namely ‘U.zeroSize’
      In the expression: C.drop (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.drop (U.size z) U.zeroSize z
    • Relevant bindings include
        r :: S.Assignment f4 b3 (bound at test/Test/Context.hs:273:13)
    |
273 |         let r = C.drop (U.size z) U.zeroSize z
    |                                   ^^^^^^^^^^

test/Test/Context.hs:273:46: error:
    • Couldn't match expected type ‘S.Assignment f4 (ctx1 <+> b3)’
                  with actual type ‘U.Assignment Payload ((x <+> x1) <+> x2)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.drop’, namely ‘z’
      In the expression: C.drop (U.size z) U.zeroSize z
      In an equation for ‘r’: r = C.drop (U.size z) U.zeroSize z
    • Relevant bindings include
        r :: S.Assignment f4 b3 (bound at test/Test/Context.hs:273:13)
        z :: U.Assignment Payload ((x <+> x1) <+> x2)
          (bound at test/Test/Context.hs:272:13)
        y :: UAsgn x2 (bound at test/Test/Context.hs:271:14)
        x :: UAsgn x1 (bound at test/Test/Context.hs:270:14)
        w :: UAsgn x (bound at test/Test/Context.hs:269:14)
    |
273 |         let r = C.drop (U.size z) U.zeroSize z
    |                                              ^

test/Test/Context.hs:274:48: error:
    • Couldn't match type ‘S.Assignment f4’
                     with ‘U.Assignment f5’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment f5 b3
        Actual type: S.Assignment f4 b3
    • In the second argument of ‘testEquality’, namely ‘r’
      In the second argument of ‘($)’, namely ‘testEquality U.empty r’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality U.empty r’
    • Relevant bindings include
        r :: S.Assignment f4 b3 (bound at test/Test/Context.hs:273:13)
    |
274 |         assert $ isJust $ testEquality U.empty r
    |                                                ^

test/Test/Context.hs:282:26: error:
    • Couldn't match expected type ‘S.Size b4’
                  with actual type ‘U.Size x’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.take’, namely ‘(U.size x)’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        x' :: S.Assignment f6 b4 (bound at test/Test/Context.hs:282:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:281:13)
        x :: UAsgn x (bound at test/Test/Context.hs:279:14)
    |
282 |         let x' = C.take (U.size x) (U.size y) z
    |                          ^^^^^^^^

test/Test/Context.hs:282:37: error:
    • Couldn't match expected type ‘S.Size ctx'2’
                  with actual type ‘U.Size x1’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.take’, namely ‘(U.size y)’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:281:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:280:14)
    |
282 |         let x' = C.take (U.size x) (U.size y) z
    |                                     ^^^^^^^^

test/Test/Context.hs:282:47: error:
    • Couldn't match expected type ‘S.Assignment f6 (b4 <+> ctx'2)’
                  with actual type ‘U.Assignment Payload (x <+> x1)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.take’, namely ‘z’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        x' :: S.Assignment f6 b4 (bound at test/Test/Context.hs:282:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:281:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:280:14)
        x :: UAsgn x (bound at test/Test/Context.hs:279:14)
    |
282 |         let x' = C.take (U.size x) (U.size y) z
    |                                               ^

test/Test/Context.hs:283:42: error:
    • Couldn't match type ‘S.Assignment f6’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b4
        Actual type: S.Assignment f6 b4
    • In the second argument of ‘testEquality’, namely ‘x'’
      In the second argument of ‘($)’, namely ‘testEquality x x'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality x x'’
    • Relevant bindings include
        x' :: S.Assignment f6 b4 (bound at test/Test/Context.hs:282:13)
    |
283 |         assert $ isJust $ testEquality x x'
    |                                          ^^

test/Test/Context.hs:291:26: error:
    • Couldn't match expected type ‘S.Size b5’
                  with actual type ‘U.Size x’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.take’, namely ‘(U.size x)’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        x' :: S.Assignment f7 b5 (bound at test/Test/Context.hs:291:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        x :: UAsgn x (bound at test/Test/Context.hs:288:14)
    |
291 |         let x' = C.take (U.size x) (U.size y) z
    |                          ^^^^^^^^

test/Test/Context.hs:291:37: error:
    • Couldn't match expected type ‘S.Size ctx'3’
                  with actual type ‘U.Size x1’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.take’, namely ‘(U.size y)’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:289:14)
    |
291 |         let x' = C.take (U.size x) (U.size y) z
    |                                     ^^^^^^^^

test/Test/Context.hs:291:47: error:
    • Couldn't match expected type ‘S.Assignment f7 (b5 <+> ctx'3)’
                  with actual type ‘U.Assignment Payload (x <+> x1)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.take’, namely ‘z’
      In the expression: C.take (U.size x) (U.size y) z
      In an equation for ‘x'’: x' = C.take (U.size x) (U.size y) z
    • Relevant bindings include
        x' :: S.Assignment f7 b5 (bound at test/Test/Context.hs:291:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:289:14)
        x :: UAsgn x (bound at test/Test/Context.hs:288:14)
    |
291 |         let x' = C.take (U.size x) (U.size y) z
    |                                               ^

test/Test/Context.hs:292:26: error:
    • Couldn't match expected type ‘S.Size ctx2’
                  with actual type ‘U.Size x’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.drop’, namely ‘(U.size x)’
      In the expression: C.drop (U.size x) (U.size y) z
      In an equation for ‘y'’: y' = C.drop (U.size x) (U.size y) z
    • Relevant bindings include
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        x :: UAsgn x (bound at test/Test/Context.hs:288:14)
    |
292 |         let y' = C.drop (U.size x) (U.size y) z
    |                          ^^^^^^^^

test/Test/Context.hs:292:37: error:
    • Couldn't match expected type ‘S.Size b6’
                  with actual type ‘U.Size x1’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.drop’, namely ‘(U.size y)’
      In the expression: C.drop (U.size x) (U.size y) z
      In an equation for ‘y'’: y' = C.drop (U.size x) (U.size y) z
    • Relevant bindings include
        y' :: S.Assignment f8 b6 (bound at test/Test/Context.hs:292:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:289:14)
    |
292 |         let y' = C.drop (U.size x) (U.size y) z
    |                                     ^^^^^^^^

test/Test/Context.hs:292:47: error:
    • Couldn't match expected type ‘S.Assignment f8 (ctx2 <+> b6)’
                  with actual type ‘U.Assignment Payload (x <+> x1)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.drop’, namely ‘z’
      In the expression: C.drop (U.size x) (U.size y) z
      In an equation for ‘y'’: y' = C.drop (U.size x) (U.size y) z
    • Relevant bindings include
        y' :: S.Assignment f8 b6 (bound at test/Test/Context.hs:292:13)
        z :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:290:13)
        y :: UAsgn x1 (bound at test/Test/Context.hs:289:14)
        x :: UAsgn x (bound at test/Test/Context.hs:288:14)
    |
292 |         let y' = C.drop (U.size x) (U.size y) z
    |                                               ^

test/Test/Context.hs:293:42: error:
    • Couldn't match type ‘S.Assignment f7’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b5
        Actual type: S.Assignment f7 b5
    • In the second argument of ‘testEquality’, namely ‘x'’
      In the second argument of ‘($)’, namely ‘testEquality x x'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality x x'’
    • Relevant bindings include
        x' :: S.Assignment f7 b5 (bound at test/Test/Context.hs:291:13)
    |
293 |         assert $ isJust $ testEquality x x'
    |                                          ^^

test/Test/Context.hs:294:42: error:
    • Couldn't match type ‘S.Assignment f8’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b6
        Actual type: S.Assignment f8 b6
    • In the second argument of ‘testEquality’, namely ‘y'’
      In the second argument of ‘($)’, namely ‘testEquality y y'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality y y'’
    • Relevant bindings include
        y' :: S.Assignment f8 b6 (bound at test/Test/Context.hs:292:13)
    |
294 |         assert $ isJust $ testEquality y y'
    |                                          ^^

test/Test/Context.hs:311:27: error:
    • Couldn't match expected type ‘S.Size b7’
                  with actual type ‘U.Size (x <+> x1)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.take’, namely ‘(U.size uv)’
      In the expression: C.take (U.size uv) (U.size wxy) z
      In an equation for ‘uv'’: uv' = C.take (U.size uv) (U.size wxy) z
    • Relevant bindings include
        uv' :: S.Assignment f9 b7 (bound at test/Test/Context.hs:311:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        v :: UAsgn x1 (bound at test/Test/Context.hs:303:14)
        u :: UAsgn x (bound at test/Test/Context.hs:302:14)
    |
311 |         let uv' = C.take (U.size uv) (U.size wxy) z
    |                           ^^^^^^^^^

test/Test/Context.hs:311:39: error:
    • Couldn't match expected type ‘S.Size ctx'4’
                  with actual type ‘U.Size ((x2 <+> x3) <+> x4)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.take’, namely ‘(U.size wxy)’
      In the expression: C.take (U.size uv) (U.size wxy) z
      In an equation for ‘uv'’: uv' = C.take (U.size uv) (U.size wxy) z
    • Relevant bindings include
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        wxy :: U.Assignment Payload ((x2 <+> x3) <+> x4)
          (bound at test/Test/Context.hs:308:13)
        y :: UAsgn x4 (bound at test/Test/Context.hs:306:14)
        x :: UAsgn x3 (bound at test/Test/Context.hs:305:14)
        w :: UAsgn x2 (bound at test/Test/Context.hs:304:14)
    |
311 |         let uv' = C.take (U.size uv) (U.size wxy) z
    |                                       ^^^^^^^^^^

test/Test/Context.hs:311:51: error:
    • Couldn't match expected type ‘S.Assignment f9 (b7 <+> ctx'4)’
                  with actual type ‘U.Assignment
                                      Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.take’, namely ‘z’
      In the expression: C.take (U.size uv) (U.size wxy) z
      In an equation for ‘uv'’: uv' = C.take (U.size uv) (U.size wxy) z
    • Relevant bindings include
        uv' :: S.Assignment f9 b7 (bound at test/Test/Context.hs:311:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        wxy :: U.Assignment Payload ((x2 <+> x3) <+> x4)
          (bound at test/Test/Context.hs:308:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        y :: UAsgn x4 (bound at test/Test/Context.hs:306:14)
        x :: UAsgn x3 (bound at test/Test/Context.hs:305:14)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
    |
311 |         let uv' = C.take (U.size uv) (U.size wxy) z
    |                                                   ^

test/Test/Context.hs:312:28: error:
    • Couldn't match expected type ‘S.Size ctx3’
                  with actual type ‘U.Size (x <+> x1)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.drop’, namely ‘(U.size uv)’
      In the expression: C.drop (U.size uv) (U.size wxy) z
      In an equation for ‘wxy'’: wxy' = C.drop (U.size uv) (U.size wxy) z
    • Relevant bindings include
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        v :: UAsgn x1 (bound at test/Test/Context.hs:303:14)
        u :: UAsgn x (bound at test/Test/Context.hs:302:14)
    |
312 |         let wxy' = C.drop (U.size uv) (U.size wxy) z
    |                            ^^^^^^^^^

test/Test/Context.hs:312:40: error:
    • Couldn't match expected type ‘S.Size b8’
                  with actual type ‘U.Size ((x2 <+> x3) <+> x4)’
      NB: ‘U.Size’ is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Size’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.drop’, namely ‘(U.size wxy)’
      In the expression: C.drop (U.size uv) (U.size wxy) z
      In an equation for ‘wxy'’: wxy' = C.drop (U.size uv) (U.size wxy) z
    • Relevant bindings include
        wxy' :: S.Assignment f11 b8 (bound at test/Test/Context.hs:312:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        wxy :: U.Assignment Payload ((x2 <+> x3) <+> x4)
          (bound at test/Test/Context.hs:308:13)
        y :: UAsgn x4 (bound at test/Test/Context.hs:306:14)
        x :: UAsgn x3 (bound at test/Test/Context.hs:305:14)
        w :: UAsgn x2 (bound at test/Test/Context.hs:304:14)
    |
312 |         let wxy' = C.drop (U.size uv) (U.size wxy) z
    |                                        ^^^^^^^^^^

test/Test/Context.hs:312:52: error:
    • Couldn't match expected type ‘S.Assignment f11 (ctx3 <+> b8)’
                  with actual type ‘U.Assignment
                                      Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the third argument of ‘C.drop’, namely ‘z’
      In the expression: C.drop (U.size uv) (U.size wxy) z
      In an equation for ‘wxy'’: wxy' = C.drop (U.size uv) (U.size wxy) z
    • Relevant bindings include
        wxy' :: S.Assignment f11 b8 (bound at test/Test/Context.hs:312:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        wxy :: U.Assignment Payload ((x2 <+> x3) <+> x4)
          (bound at test/Test/Context.hs:308:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        y :: UAsgn x4 (bound at test/Test/Context.hs:306:14)
        x :: UAsgn x3 (bound at test/Test/Context.hs:305:14)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
    |
312 |         let wxy' = C.drop (U.size uv) (U.size wxy) z
    |                                                    ^

test/Test/Context.hs:313:36: error:
    • Couldn't match expected type ‘S.Assignment f10 xs0’
                  with actual type ‘U.Assignment
                                      Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the first argument of ‘C.dropPrefix’, namely ‘z’
      In the expression: C.dropPrefix z uv (error "failed dropPrefix")
      In an equation for ‘withWXY’:
          withWXY = C.dropPrefix z uv (error "failed dropPrefix")
    • Relevant bindings include
        withWXY :: (forall (addl :: Ctx k6).
                    (xs0 ~ (prefix0 <+> addl)) =>
                    S.Assignment f10 addl -> PropertyT IO ())
                   -> PropertyT IO ()
          (bound at test/Test/Context.hs:313:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        wxy :: U.Assignment Payload ((x2 <+> x3) <+> x4)
          (bound at test/Test/Context.hs:308:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        y :: UAsgn x4 (bound at test/Test/Context.hs:306:14)
        x :: UAsgn x3 (bound at test/Test/Context.hs:305:14)
        (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
    |
313 |         let withWXY = C.dropPrefix z uv (error "failed dropPrefix")
    |                                    ^

test/Test/Context.hs:313:38: error:
    • Couldn't match expected type ‘S.Assignment f10 prefix0’
                  with actual type ‘U.Assignment Payload (x <+> x1)’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
    • In the second argument of ‘C.dropPrefix’, namely ‘uv’
      In the expression: C.dropPrefix z uv (error "failed dropPrefix")
      In an equation for ‘withWXY’:
          withWXY = C.dropPrefix z uv (error "failed dropPrefix")
    • Relevant bindings include
        withWXY :: (forall (addl :: Ctx k6).
                    (xs0 ~ (prefix0 <+> addl)) =>
                    S.Assignment f10 addl -> PropertyT IO ())
                   -> PropertyT IO ()
          (bound at test/Test/Context.hs:313:13)
        z :: U.Assignment Payload ((x <+> x1) <+> ((x2 <+> x3) <+> x4))
          (bound at test/Test/Context.hs:310:13)
        uv :: U.Assignment Payload (x <+> x1)
          (bound at test/Test/Context.hs:307:13)
        v :: UAsgn x1 (bound at test/Test/Context.hs:303:14)
        u :: UAsgn x (bound at test/Test/Context.hs:302:14)
    |
313 |         let withWXY = C.dropPrefix z uv (error "failed dropPrefix")
    |                                      ^^

test/Test/Context.hs:314:53: error:
    • Couldn't match type ‘S.Assignment f9’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b7
        Actual type: S.Assignment f9 b7
    • In the second argument of ‘testEquality’, namely ‘uv'’
      In the second argument of ‘($)’, namely
        ‘testEquality (u U.<++> v) uv'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality (u U.<++> v) uv'’
    • Relevant bindings include
        uv' :: S.Assignment f9 b7 (bound at test/Test/Context.hs:311:13)
    |
314 |         assert $ isJust $ testEquality (u U.<++> v) uv'
    |                                                     ^^^

test/Test/Context.hs:315:62: error:
    • Couldn't match type ‘S.Assignment f11’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b8
        Actual type: S.Assignment f11 b8
    • In the second argument of ‘testEquality’, namely ‘wxy'’
      In the second argument of ‘($)’, namely
        ‘testEquality (w U.<++> x U.<++> y) wxy'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality (w U.<++> x U.<++> y) wxy'’
    • Relevant bindings include
        wxy' :: S.Assignment f11 b8 (bound at test/Test/Context.hs:312:13)
    |
315 |         assert $ isJust $ testEquality (w U.<++> x U.<++> y) wxy'
    |                                                              ^^^^

test/Test/Context.hs:316:43: error:
    • Couldn't match type ‘S.Assignment f9’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b7
        Actual type: S.Assignment f9 b7
    • In the second argument of ‘testEquality’, namely ‘uv'’
      In the second argument of ‘($)’, namely ‘testEquality uv uv'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality uv uv'’
    • Relevant bindings include
        uv' :: S.Assignment f9 b7 (bound at test/Test/Context.hs:311:13)
    |
316 |         assert $ isJust $ testEquality uv uv'
    |                                           ^^^

test/Test/Context.hs:317:44: error:
    • Couldn't match type ‘S.Assignment f11’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b8
        Actual type: S.Assignment f11 b8
    • In the second argument of ‘testEquality’, namely ‘wxy'’
      In the second argument of ‘($)’, namely ‘testEquality wxy wxy'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality wxy wxy'’
    • Relevant bindings include
        wxy' :: S.Assignment f11 b8 (bound at test/Test/Context.hs:312:13)
    |
317 |         assert $ isJust $ testEquality wxy wxy'
    |                                            ^^^^

test/Test/Context.hs:318:61: error:
    • Could not deduce: addl ~~ b9
      from the context: xs0 ~ (prefix0 <+> addl)
        bound by a type expected by the context:
                   forall (addl :: Ctx k6).
                   (xs0 ~ (prefix0 <+> addl)) =>
                   S.Assignment f10 addl -> PropertyT IO ()
        at test/Test/Context.hs:318:19-61
      ‘addl’ is a rigid type variable bound by
        a type expected by the context:
          forall (addl :: Ctx k6).
          (xs0 ~ (prefix0 <+> addl)) =>
          S.Assignment f10 addl -> PropertyT IO ()
        at test/Test/Context.hs:318:19-61
      Expected type: S.Assignment f11 b9
        Actual type: S.Assignment f10 addl
    • In the second argument of ‘testEquality’, namely ‘t’
      In the second argument of ‘($)’, namely ‘testEquality wxy' t’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality wxy' t’
    • Relevant bindings include
        t :: S.Assignment f10 addl (bound at test/Test/Context.hs:318:20)
        withWXY :: (forall (addl :: Ctx k6).
                    (xs0 ~ (prefix0 <+> addl)) =>
                    S.Assignment f10 addl -> PropertyT IO ())
                   -> PropertyT IO ()
          (bound at test/Test/Context.hs:313:13)
    |
318 |         withWXY $ \t -> assert $ isJust $ testEquality wxy' t
    |                                                             ^

test/Test/Context.hs:322:37: error:
    • Couldn't match type ‘U.Assignment Payload x’
                     with ‘S.Assignment f12 b10’
      NB: ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
          ‘U.Assignment’ is defined in ‘Data.Parameterized.Context.Unsafe’
      Expected type: S.Assignment f12 b10
        Actual type: UAsgn x
    • In the second argument of ‘S.zipWith’, namely ‘x’
      In the expression: S.zipWith Pair x x
      In an equation for ‘zipped’: zipped = S.zipWith Pair x x
    • Relevant bindings include
        zipped :: S.Assignment (Product f12 g0) b10
          (bound at test/Test/Context.hs:322:13)
        x :: UAsgn x (bound at test/Test/Context.hs:321:14)
    |
322 |         let zipped = C.zipWith Pair x x
    |                                     ^

test/Test/Context.hs:322:39: error:
    • Couldn't match type ‘U.Assignment Payload x’
                     with ‘S.Assignment g0 b10’
      NB: ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
          ‘U.Assignment’ is defined in ‘Data.Parameterized.Context.Unsafe’
      Expected type: S.Assignment g0 b10
        Actual type: UAsgn x
    • In the third argument of ‘S.zipWith’, namely ‘x’
      In the expression: S.zipWith Pair x x
      In an equation for ‘zipped’: zipped = S.zipWith Pair x x
    • Relevant bindings include
        zipped :: S.Assignment (Product f12 g0) b10
          (bound at test/Test/Context.hs:322:13)
        x :: UAsgn x (bound at test/Test/Context.hs:321:14)
    |
322 |         let zipped = C.zipWith Pair x x
    |                                       ^

test/Test/Context.hs:324:42: error:
    • Couldn't match type ‘S.Assignment f12’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b10
        Actual type: S.Assignment f12 b10
    • In the second argument of ‘testEquality’, namely ‘x'’
      In the second argument of ‘($)’, namely ‘testEquality x x'’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality x x'’
    • Relevant bindings include
        x' :: S.Assignment f12 b10 (bound at test/Test/Context.hs:323:14)
        zipped :: S.Assignment (Product f12 g0) b10
          (bound at test/Test/Context.hs:322:13)
    |
324 |         assert $ isJust $ testEquality x x'
    |                                          ^^

test/Test/Context.hs:325:42: error:
    • Couldn't match type ‘S.Assignment g0’
                     with ‘U.Assignment Payload’
      NB: ‘U.Assignment’
            is defined in ‘Data.Parameterized.Context.Unsafe’
          ‘S.Assignment’ is defined in ‘Data.Parameterized.Context.Safe’
      Expected type: U.Assignment Payload b10
        Actual type: S.Assignment g0 b10
    • In the second argument of ‘testEquality’, namely ‘x''’
      In the second argument of ‘($)’, namely ‘testEquality x x''’
      In the second argument of ‘($)’, namely
        ‘isJust $ testEquality x x''’
    • Relevant bindings include
        x'' :: S.Assignment g0 b10 (bound at test/Test/Context.hs:323:18)
        zipped :: S.Assignment (Product f12 g0) b10
          (bound at test/Test/Context.hs:322:13)
    |
325 |         assert $ isJust $ testEquality x x''
    |                                          ^^^