Better inference for AppendIndices (well-typed#451)

* Better inference for AppendIndices * Allow the second argument of `AppendIndices` to be determined by the first and third arguments. * Refine the documentation for `AppendIndices`. Due to the way incoherent instances work, the "short-circuit" path is actually treated as a fall-back; it will *only* be taken if nothing is known about the shape of the first list. * Update optics-core/src/Optics/Internal/Optic/TypeLevel.hs Co-authored-by: Andrzej Rybczak <[email protected]> Co-authored-by: Andrzej Rybczak <[email protected]>
IaFP · Mar 23, 2022 · a130506 · a130506
1 parent 54cf982
commit a130506
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/optics-core/src/Optics/Internal/Optic/TypeLevel.hs b/optics-core/src/Optics/Internal/Optic/TypeLevel.hs
@@ -111,12 +111,12 @@ data IxEq i is js where
 class AppendIndices xs ys ks | xs ys -> ks where
   appendIndices :: IxEq i (Curry xs (Curry ys i)) (Curry ks i)
 
--- | If the second list is empty, we can shortcircuit and pick the first list
--- immediately.
-instance {-# INCOHERENT #-} AppendIndices xs '[] xs where
+-- | If the second list is empty, we can pick the first list
+-- even if nothing is known about it.
+instance {-# INCOHERENT #-} xs ~ zs => AppendIndices xs '[] zs where
   appendIndices = IxEq
 
-instance AppendIndices '[] ys ys where
+instance ys ~ zs => AppendIndices '[] ys zs where
   appendIndices = IxEq
 
 instance AppendIndices xs ys ks => AppendIndices (x ': xs) ys (x ': ks) where