Do not pass deps to mkUnivCo

src-ghc-9.12/GHC/TypeLits/Normalise.hs

@@ -706,17 +706,17 @@ evSubtPreds :: CtLoc -> [PredType] -> TcPluginM [Ct]
 evSubtPreds loc = mapM (fmap mkNonCanonical . newWanted loc)
 
 evMagic :: Ct -> [Coercion] -> Set CType -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
-evMagic ct deps knW preds = do
+evMagic ct _deps knW preds = do
   holeWanteds <- evSubtPreds (ctLoc ct) preds
   knWanted <- mapM (mkKnWanted (ctLoc ct)) (toList knW)
   let newWant = knWanted ++ holeWanteds
   case classifyPredType $ ctEvPred $ ctEvidence ct of
     EqPred NomEq t1 t2 ->
-      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Nominal t1 t2
+      let ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") [] Nominal t1 t2
       in return (Just ((EvExpr (Coercion ctEv), ct),newWant))
     IrredPred p ->
       let t1 = mkTyConApp (cTupleTyCon 0) []
-          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") deps Representational t1 p
+          co = mkUnivCo (PluginProv "ghc-typelits-natnormalise") [] Representational t1 p
           dcApp = evId (dataConWrapId (cTupleDataCon 0))
        in return (Just ((evCast dcApp co, ct),newWant))
     _ -> return Nothing

tests/Tests.hs

@@ -245,6 +245,31 @@ merge :: Vec n a -> Vec n a -> Vec (n + n) a
 merge Nil       Nil       = Nil
 merge (x :> xs) (y :> ys) = x :> y :> merge xs ys
 
+-- | \"'select' @f s n xs@\" selects /n/ elements with step-size /s/ and
+-- offset @f@ from /xs/.
+--
+-- >>> select (SNat :: SNat 1) (SNat :: SNat 2) (SNat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
+-- 2 :> 4 :> 6 :> Nil
+-- >>> select d1 d2 d3 (1:>2:>3:>4:>5:>6:>7:>8:>Nil)
+-- 2 :> 4 :> 6 :> Nil
+select :: forall i s n f a. s * n + 1 <= i + s
+       => SNat f
+       -> SNat s
+       -> SNat n
+       -> Vec (f + i) a
+       -> Vec n a
+select f s n xs = select' (toUNat n) $ drop f xs
+ where
+  select' :: forall m j b. (s * m + 1 <= j + s) => UNat m -> Vec j b -> Vec m b
+  select' m vs = case m of
+    UZero -> Nil
+    USucc UZero -> head @(j - 1) vs :> Nil
+    USucc m'@(USucc _) -> case deduce @(s * (m - 1) + 1) @j Proxy Proxy of
+      Dict -> head @(j - 1) vs :> select' m' (drop @s @(j - s) s vs)
+
+  deduce :: e + s <= k + s => p e -> p k -> Dict (e <= k)
+  deduce _ _ = Dict
+
 -- | 'drop' @n xs@ returns the suffix of @xs@ after the first @n@ elements
 --
 -- >>> drop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil)