From 22a3d9c5cbafb7a633f2f802af884d042718e78d Mon Sep 17 00:00:00 2001 From: Mikolaj Konarski Date: Wed, 24 Sep 2025 20:56:20 +0200 Subject: Port to ghc-typelits-natnormalise-0.8.1 that is much overhauled and probably more sound than earlier versions. --- src/Data/Array/Nested/Lemmas.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src/Data/Array/Nested/Lemmas.hs') diff --git a/src/Data/Array/Nested/Lemmas.hs b/src/Data/Array/Nested/Lemmas.hs index 8cac298..e089479 100644 --- a/src/Data/Array/Nested/Lemmas.hs +++ b/src/Data/Array/Nested/Lemmas.hs @@ -43,14 +43,18 @@ lemAppLeft _ Refl = Refl lemReplicatePlusApp :: forall n m a. SNat n -> Proxy m -> Proxy a -> Replicate (n + m) a :~: Replicate n a ++ Replicate m a +{- for now, the plugins can't derive a type for this code, see + https://github.com/clash-lang/ghc-typelits-natnormalise/pull/98#issuecomment-3332842214 lemReplicatePlusApp sn _ _ = go sn where go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a go SZ = Refl go (SS (n :: SNat n'm1)) - | Refl <- lemReplicateSucc @a @n'm1 + | Refl <- lemReplicateSucc @a n , Refl <- go n - = sym (lemReplicateSucc @a @(n'm1 + m)) + = sym (lemReplicateSucc @a (SNat @(n'm1 + m))) +-} +lemReplicatePlusApp _ _ _ = unsafeCoerceRefl lemDropLenApp :: Rank l1 <= Rank l2 => Proxy l1 -> Proxy l2 -> Proxy rest -- cgit v1.2.3-70-g09d2