summaryrefslogtreecommitdiff
path: root/Algebra/Internal.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Algebra/Internal.hs')
-rw-r--r--Algebra/Internal.hs6
1 files changed, 4 insertions, 2 deletions
diff --git a/Algebra/Internal.hs b/Algebra/Internal.hs
index 0464e74..2f1a358 100644
--- a/Algebra/Internal.hs
+++ b/Algebra/Internal.hs
@@ -3,7 +3,7 @@
{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -Wincomplete-patterns -Wno-orphans #-}
module Algebra.Internal
( (:~:)(..), withRefl,
module Data.Proxy,
@@ -41,6 +41,7 @@ import Data.Type.Equality ((:~:) (..))
import Data.Type.Natural.Class as Algebra.Internal
import qualified Data.Type.Ordinal as O
import qualified Data.Vector as DV
+import Data.ListLike (ListLike)
import GHC.TypeLits as Algebra.Internal
import Proof.Equational (coerce, withRefl)
import Proof.Equational as Algebra.Internal (because,
@@ -64,7 +65,8 @@ coerceLength eql = _Unwrapping Flipped.Flipped %~ coerce eql
type SNat (n :: Nat) = Sing n
-sizedLength f = (S.sLength f)
+sizedLength :: ListLike (f a) a => S.Sized f n a -> Sing n
+sizedLength f = S.sLength f
padVecs :: forall a n m. a -> Sized' n a -> Sized' m a
-> (SNat (Max n m), Sized' (Max n m) a, Sized' (Max n m) a)