{-# OPTIONS_HADDOCK hide, prune #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
module Data.Type.List.Classes
(
SnocList, ReverseList, ConcatList
, inferStripSuffix, inferStripPrefix, inferConcat
, nilInstSnocList, consInstSnocList, incohInstSnocList
, consInstReverseList, incohInstReverseList
, nilInstConcatList, consInstConcatList, incohInstConcatList
) where
import Data.Constraint (Dict (..))
import Data.Constraint.Bare
import Data.Constraint.Deriving
import Data.Kind
import Data.Type.Equality
import Unsafe.Coerce (unsafeCoerce)
import Data.Type.List.Families
import Data.Type.List.Internal
class
( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs
, SnocListCtx as a bs, ConcatList as '[a] bs)
=> SnocList (as :: [k]) (a :: k) (bs :: [k])
| as a -> bs, bs -> as a, as -> k, a -> a, bs -> k where
class
( as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as
, ReverseListCtx as bs)
=> ReverseList (as :: [k]) (bs :: [k])
| as -> bs, bs -> as, as -> k, bs -> k
class
( asbs ~ Concat as bs
, as ~ StripSuffix bs asbs
, bs ~ StripPrefix as asbs
, ConcatListCtx1 as bs asbs
, ConcatListCtx2 as bs asbs (bs == asbs)
) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])
| as bs -> asbs, as asbs -> bs
, as -> k, bs -> k, asbs -> k
type family SnocListCtx (as :: [k]) (a :: k) (bs :: [k]) :: Constraint where
SnocListCtx '[] z bs =
( Head bs ~ z
, Tail bs ~ '[]
, bs ~ '[z]
, UnreachableConstraint (SnocList (Tail '[]) (Head '[]) (Tail bs))
"SnocListCtx '[] z bs -- SnocList (Tail '[]) (Head '[]) (Tail bs)"
)
SnocListCtx (a ': as) z bs =
( Head bs ~ a
, Tail bs ~ Snoc as z
, bs ~ (Head bs ': Head (Tail bs) ': Tail (Tail bs))
, SnocList as z (Tail bs)
)
type family ReverseListCtx (as :: [k]) (bs :: [k]) :: Constraint where
ReverseListCtx '[] bs =
( bs ~ '[]
, UnreachableConstraint (ReverseList (Tail '[]) (Init bs))
"ReverseListCtx '[] bs -- ReverseList (Tail '[]) (Init bs)"
, UnreachableConstraint (SnocList (Init bs) (Head '[]) bs)
"ReverseListCtx '[] bs -- SnocList (Init bs) (Head '[]) bs"
)
ReverseListCtx (a ': as) bs =
( bs ~ (Head bs ': Tail bs)
, ReverseList as (Init bs)
, SnocList (Init bs) a bs
)
type family ConcatListCtx1 (as :: [k]) (bs :: [k]) (asbs :: [k]) :: Constraint where
ConcatListCtx1 '[] bs asbs =
( asbs ~ bs
, (bs == asbs) ~ 'True
, UnreachableConstraint (Head '[] ~ Head asbs)
"ConcatListCtx1 '[] bs asbs -- (Head '[] ~ Head asbs)"
, UnreachableConstraint (ConcatList (Tail '[]) bs (Tail asbs))
"ConcatListCtx1 '[] bs asbs -- ConcatList (Tail '[]) bs (Tail asbs)"
, UnreachableConstraint (ConcatList (Init '[]) (Last '[] ': bs) asbs)
"ConcatListCtx1 '[] bs asbs -- ConcatList (Init '[]) (Last '[] ': bs) asbs"
)
ConcatListCtx1 (a ': as) bs asbs =
( asbs ~ (a ': Tail asbs)
, (bs == asbs) ~ 'False
, a ~ Head asbs
, ConcatList as bs (Tail asbs)
, ConcatList (Init (a ': as)) (Last (a ': as) ': bs) asbs
)
type family ConcatListCtx2 (as :: [k]) (bs :: [k]) (asbs :: [k]) (bsEq :: Bool) :: Constraint where
ConcatListCtx2 as bs asbs 'True =
( as ~ '[]
, bs ~ asbs
, UnreachableConstraint (ConcatList (Tail as) bs (Tail asbs))
"ConcatListCtx2 as bs asbs 'True -- ConcatList (Tail as) bs (Tail asbs)"
)
ConcatListCtx2 as bs (a ': asbs) 'False =
( as ~ (a ': Tail as)
, a ~ Head as
, ConcatList (Tail as) bs asbs
)
ConcatListCtx2 as bs '[] _ =
( as ~ '[]
, bs ~ '[]
, UnreachableConstraint (ConcatList (Tail as) bs (Tail '[]))
"ConcatListCtx2 as bs '[] _ -- ConcatList (Tail as) bs (Tail '[])"
)
{-# ANN defineSnocList ClassDict #-}
defineSnocList :: forall (k :: Type) (as :: [k]) (a :: k) (bs :: [k])
. ( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs
, SnocListCtx as a bs
, ConcatList as '[a] bs
)
=> Dict (SnocList as a bs)
defineSnocList :: Dict (SnocList as a bs)
defineSnocList = Dict (SnocList as a bs)
forall k (as :: [k]) (a :: k) (bs :: [k]).
(bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs,
ConcatList as '[a] bs) =>
Dict (SnocList as a bs)
defineSnocList
{-# ANN defineReverseList ClassDict #-}
defineReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs)
=> Dict (ReverseList as bs)
defineReverseList :: Dict (ReverseList as bs)
defineReverseList = Dict (ReverseList as bs)
forall k (as :: [k]) (bs :: [k]).
(as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as,
ReverseListCtx as bs) =>
Dict (ReverseList as bs)
defineReverseList
{-# ANN defineConcatList ClassDict #-}
defineConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. ( asbs ~ Concat as bs
, as ~ StripSuffix bs asbs
, bs ~ StripPrefix as asbs
, ConcatListCtx1 as bs asbs
, ConcatListCtx2 as bs asbs (bs == asbs)
)
=> Dict (ConcatList as bs asbs)
defineConcatList :: Dict (ConcatList as bs asbs)
defineConcatList = Dict (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
(asbs ~ Concat as bs, as ~ StripSuffix bs asbs,
bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs,
ConcatListCtx2 as bs asbs (bs == asbs)) =>
Dict (ConcatList as bs asbs)
defineConcatList
unsafeBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])
. BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
unsafeBareSnocList :: BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
unsafeBareSnocList = (SnocListCtx as z bs =-> BareConstraint (SnocList as z bs))
-> BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)
m
where
m :: SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)
m :: SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)
m | Dict (bs ~ Snoc as z)
Dict <- Dict (bs ~ Snoc as z)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @bs @(Snoc as z)
, Dict (as ~ Init bs)
Dict <- Dict (as ~ Init bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @as @(Init bs)
, Dict (z ~ Last bs)
Dict <- Dict (z ~ Last bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @z @(Last bs)
, Dict (bs ~ Concat as '[z])
Dict <- Dict (bs ~ Concat as '[z])
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @bs @(Concat as '[z])
, Dict (ConcatList as '[z] bs)
Dict <- (bs ~ Concat as '[z]) => Dict (ConcatList as '[z] bs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
(asbs ~ Concat as bs) =>
Dict (ConcatList as bs asbs)
inferConcat @as @'[z] @bs
= (SnocListCtx as z bs => BareConstraint (SnocList as z bs))
-> SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (SnocList as z bs) -> BareConstraint (SnocList as z bs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare (Dict (SnocList as z bs) -> BareConstraint (SnocList as z bs))
-> Dict (SnocList as z bs) -> BareConstraint (SnocList as z bs)
forall a b. (a -> b) -> a -> b
$ (bs ~ Snoc as z, as ~ Init bs, z ~ Last bs, SnocListCtx as z bs,
ConcatList as '[z] bs) =>
Dict (SnocList as z bs)
forall k (as :: [k]) (a :: k) (bs :: [k]).
(bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs,
ConcatList as '[a] bs) =>
Dict (SnocList as a bs)
defineSnocList @k @as @z @bs)
unsafeBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. BareConstraint (ReverseList bs as)
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
unsafeBareReverseList :: BareConstraint (ReverseList bs as)
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
unsafeBareReverseList = (ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ((ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs))
-> (BareConstraint (ReverseList bs as)
-> ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
-> BareConstraint (ReverseList bs as)
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReverseList bs as
=-> (ReverseListCtx as bs =-> BareConstraint (ReverseList as bs)))
-> BareConstraint (ReverseList bs as)
-> ReverseListCtx as bs =-> BareConstraint (ReverseList as bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ReverseList bs as
=-> (ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
m
where
m :: ReverseList bs as
=-> ReverseListCtx as bs
=-> BareConstraint (ReverseList as bs)
m :: ReverseList bs as
=-> (ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
m | Dict (as ~ Reverse bs)
Dict <- Dict (as ~ Reverse bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @as @(Reverse bs)
, Dict (bs ~ Reverse as)
Dict <- Dict (bs ~ Reverse as)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @bs @(Reverse as)
= (ReverseList bs as =>
ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
-> ReverseList bs as
=-> (ReverseListCtx as bs =-> BareConstraint (ReverseList as bs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic ((ReverseListCtx as bs => BareConstraint (ReverseList as bs))
-> ReverseListCtx as bs =-> BareConstraint (ReverseList as bs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ReverseList as bs) -> BareConstraint (ReverseList as bs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare (Dict (ReverseList as bs) -> BareConstraint (ReverseList as bs))
-> Dict (ReverseList as bs) -> BareConstraint (ReverseList as bs)
forall a b. (a -> b) -> a -> b
$ (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as,
ReverseListCtx as bs) =>
Dict (ReverseList as bs)
forall k (as :: [k]) (bs :: [k]).
(as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as,
ReverseListCtx as bs) =>
Dict (ReverseList as bs)
defineReverseList @k @as @bs))
unsafeBareConcatList ::
forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. BareConstraint (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
unsafeBareConcatList :: BareConstraint (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
unsafeBareConcatList = (ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ((ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs))
-> (BareConstraint (ConcatListCtx1 as bs asbs)
-> ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
-> BareConstraint (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcatListCtx1 as bs asbs
=-> (ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs)))
-> BareConstraint (ConcatListCtx1 as bs asbs)
-> ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ConcatListCtx1 as bs asbs
=-> (ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
m
where
m :: ConcatListCtx1 as bs asbs
=-> ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs)
m :: ConcatListCtx1 as bs asbs
=-> (ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
m | Dict (as ~ StripSuffix bs asbs)
Dict <- Dict (as ~ StripSuffix bs asbs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @as @(StripSuffix bs asbs)
, Dict (bs ~ StripPrefix as asbs)
Dict <- Dict (bs ~ StripPrefix as asbs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @bs @(StripPrefix as asbs)
, Dict (asbs ~ Concat as bs)
Dict <- Dict (asbs ~ Concat as bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @asbs @(Concat as bs)
= (ConcatListCtx1 as bs asbs =>
ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
-> ConcatListCtx1 as bs asbs
=-> (ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic ((ConcatListCtx2 as bs asbs (bs == asbs) =>
BareConstraint (ConcatList as bs asbs))
-> ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ConcatList as bs asbs)
-> BareConstraint (ConcatList as bs asbs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare (Dict (ConcatList as bs asbs)
-> BareConstraint (ConcatList as bs asbs))
-> Dict (ConcatList as bs asbs)
-> BareConstraint (ConcatList as bs asbs)
forall a b. (a -> b) -> a -> b
$ (asbs ~ Concat as bs, as ~ StripSuffix bs asbs,
bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs,
ConcatListCtx2 as bs asbs (bs == asbs)) =>
Dict (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
(asbs ~ Concat as bs, as ~ StripSuffix bs asbs,
bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs,
ConcatListCtx2 as bs asbs (bs == asbs)) =>
Dict (ConcatList as bs asbs)
defineConcatList @k @as @bs @asbs))
unsafeBareSnocListCtx :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])
. BareConstraint (SnocList (Tail as) z (Tail bs))
-> BareConstraint (SnocListCtx as z bs)
unsafeBareSnocListCtx :: BareConstraint (SnocList (Tail as) z (Tail bs))
-> BareConstraint (SnocListCtx as z bs)
unsafeBareSnocListCtx = (SnocList (Tail as) z (Tail bs)
=-> BareConstraint (SnocListCtx as z bs))
-> BareConstraint (SnocList (Tail as) z (Tail bs))
-> BareConstraint (SnocListCtx as z bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic SnocList (Tail as) z (Tail bs)
=-> BareConstraint (SnocListCtx as z bs)
m
where
m :: SnocList (Tail as) z (Tail bs) =-> BareConstraint (SnocListCtx as z bs)
m :: SnocList (Tail as) z (Tail bs)
=-> BareConstraint (SnocListCtx as z bs)
m = (SnocList (Tail as) z (Tail bs) =>
BareConstraint (SnocListCtx as z bs))
-> SnocList (Tail as) z (Tail bs)
=-> BareConstraint (SnocListCtx as z bs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (SnocListCtx as z bs) -> BareConstraint (SnocListCtx as z bs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (SnocListCtx as z bs)
SnocList (Tail as) z (Tail bs) => Dict (SnocListCtx as z bs)
d)
d :: SnocList (Tail as) z (Tail bs) => Dict (SnocListCtx as z bs)
d :: Dict (SnocListCtx as z bs)
d = Dict
(Head as ~ Head as, Concat (Tail as) '[z] ~ Concat (Tail as) '[z],
bs ~ bs,
SnocList (StripSuffix '[z] (Tail bs)) z (Concat (Tail as) '[z]))
-> Dict (SnocListCtx as z bs)
forall a b. a -> b
unsafeCoerce (Dict
(Head as ~ Head as, Concat (Tail as) '[z] ~ Concat (Tail as) '[z],
bs ~ bs,
SnocList (StripSuffix '[z] (Tail bs)) z (Concat (Tail as) '[z]))
-> Dict (SnocListCtx as z bs))
-> Dict
(Head as ~ Head as, Concat (Tail as) '[z] ~ Concat (Tail as) '[z],
bs ~ bs,
SnocList (StripSuffix '[z] (Tail bs)) z (Concat (Tail as) '[z]))
-> Dict (SnocListCtx as z bs)
forall a b. (a -> b) -> a -> b
$ (Head as ~ Head as, Tail bs ~ Tail bs, bs ~ bs,
SnocList (Tail as) z (Tail bs)) =>
Dict
(Head as ~ Head as, Tail bs ~ Tail bs, bs ~ bs,
SnocList (Tail as) z (Tail bs))
forall (a :: Constraint). a => Dict a
Dict
@(Head as ~ Head as, Tail bs ~ Tail bs, bs ~ bs, SnocList (Tail as) z (Tail bs))
unsafeBareReverseListCtx :: forall (k :: Type) (as :: [k]) (bs :: [k])
. BareConstraint (ReverseList (Tail as) (Init bs))
-> BareConstraint (ReverseListCtx as bs)
unsafeBareReverseListCtx :: BareConstraint (ReverseList (Tail as) (Init bs))
-> BareConstraint (ReverseListCtx as bs)
unsafeBareReverseListCtx
= (ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs))
-> BareConstraint (ReverseList (Tail as) (Init bs))
-> BareConstraint (ReverseListCtx as bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ((SnocList (Init bs) (Head as) bs
=-> (ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs)))
-> BareConstraint (SnocList (Init bs) (Head as) bs)
-> ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic SnocList (Init bs) (Head as) bs
=-> (ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs))
m BareConstraint (SnocList (Init bs) (Head as) bs)
forall k (as :: [k]) (z :: k) (bs :: [k]).
BareConstraint (SnocList as z bs)
unsafeIncohBareSnocList)
where
m :: SnocList (Init bs) (Head as) bs
=-> ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs)
m :: SnocList (Init bs) (Head as) bs
=-> (ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs))
m = (SnocList (Init bs) (Head as) bs =>
ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs))
-> SnocList (Init bs) (Head as) bs
=-> (ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic ((ReverseList (Tail as) (StripSuffix '[Last bs] bs) =>
BareConstraint (ReverseListCtx as bs))
-> ReverseList (Tail as) (StripSuffix '[Last bs] bs)
=-> BareConstraint (ReverseListCtx as bs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ReverseListCtx as bs)
-> BareConstraint (ReverseListCtx as bs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (ReverseListCtx as bs)
(SnocList (Init bs) (Last bs) bs,
ReverseList (Tail as) (Init bs)) =>
Dict (ReverseListCtx as bs)
f))
f :: ( SnocList (Init bs) (Last bs) bs
, ReverseList (Tail as) (Init bs)
)
=> Dict (ReverseListCtx as bs)
f :: Dict (ReverseListCtx as bs)
f | Dict (Head as ~ Last bs)
Dict <- Dict (Head as ~ Last bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(Head as) @(Last bs)
= Dict
(bs ~ bs,
ReverseList
(RunList (Reverse' (StripSuffix '[Last bs] bs)))
(RunList (Reverse' (Tail as))),
SnocList (RunList (Reverse' (Tail as))) (Last bs) bs)
-> Dict (ReverseListCtx as bs)
forall a b. a -> b
unsafeCoerce (
(bs ~ bs, ReverseList (Tail as) (Init bs),
SnocList (Init bs) (Head as) bs) =>
Dict
(bs ~ bs, ReverseList (Tail as) (Init bs),
SnocList (Init bs) (Head as) bs)
forall (a :: Constraint). a => Dict a
Dict @( bs ~ bs
, ReverseList (Tail as) (Init bs)
, SnocList (Init bs) (Head as) bs)
)
unsafeBareConcatListCtx1 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatList (Init as) (Last as ': bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
unsafeBareConcatListCtx1 :: BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
unsafeBareConcatListCtx1 = (ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ((ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs))
-> (BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
-> BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcatList (Tail as) bs (Tail asbs)
=-> (ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs)))
-> BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs)
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ConcatList (Tail as) bs (Tail asbs)
=-> (ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
m
where
m :: ConcatList (Tail as) bs (Tail asbs)
=-> ConcatList (Init as) (Last as ': bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs)
m :: ConcatList (Tail as) bs (Tail asbs)
=-> (ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
m = (ConcatList (Tail as) bs (Tail asbs) =>
ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
-> ConcatList (Tail as) bs (Tail asbs)
=-> (ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic ((ConcatList (Init as) (Last as : bs) asbs =>
BareConstraint (ConcatListCtx1 as bs asbs))
-> ConcatList (Init as) (Last as : bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs)
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (ConcatListCtx1 as bs asbs)
(ConcatList (Tail as) bs (Tail asbs),
ConcatList (Init as) (Last as : bs) asbs) =>
Dict (ConcatListCtx1 as bs asbs)
d))
d :: ( ConcatList (Tail as) bs (Tail asbs)
, ConcatList (Init as) (Last as ': bs) asbs)
=> Dict (ConcatListCtx1 as bs asbs)
d :: Dict (ConcatListCtx1 as bs asbs)
d = Dict
(asbs ~ asbs, (bs == asbs) ~ (bs == asbs), Head asbs ~ Head asbs,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs),
ConcatList (StripSuffix (Last as : bs) asbs) (Last as : bs) asbs)
-> Dict (ConcatListCtx1 as bs asbs)
forall a b. a -> b
unsafeCoerce (Dict
(asbs ~ asbs, (bs == asbs) ~ (bs == asbs), Head asbs ~ Head asbs,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs),
ConcatList (StripSuffix (Last as : bs) asbs) (Last as : bs) asbs)
-> Dict (ConcatListCtx1 as bs asbs))
-> Dict
(asbs ~ asbs, (bs == asbs) ~ (bs == asbs), Head asbs ~ Head asbs,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs),
ConcatList (StripSuffix (Last as : bs) asbs) (Last as : bs) asbs)
-> Dict (ConcatListCtx1 as bs asbs)
forall a b. (a -> b) -> a -> b
$ (asbs ~ asbs, (bs == asbs) ~ (bs == asbs), Head asbs ~ Head asbs,
ConcatList (Tail as) bs (Tail asbs),
ConcatList (Init as) (Last as : bs) asbs) =>
Dict
(asbs ~ asbs, (bs == asbs) ~ (bs == asbs), Head asbs ~ Head asbs,
ConcatList (Tail as) bs (Tail asbs),
ConcatList (Init as) (Last as : bs) asbs)
forall (a :: Constraint). a => Dict a
Dict
@( asbs ~ asbs, (bs == asbs) ~ (bs == asbs)
, Head asbs ~ Head asbs
, ConcatList (Tail as) bs (Tail asbs)
, ConcatList (Init as) (Last as ': bs) asbs
)
unsafeBareConcatListCtx2 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
unsafeBareConcatListCtx2 :: BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
unsafeBareConcatListCtx2 = (ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs)))
-> BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
m
where
m :: ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
m :: ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
m = (ConcatList (Tail as) bs (Tail asbs) =>
BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs)))
-> ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (ConcatListCtx2 as bs asbs (bs == asbs))
ConcatList (Tail as) bs (Tail asbs) =>
Dict (ConcatListCtx2 as bs asbs (bs == asbs))
d)
d :: ConcatList (Tail as) bs (Tail asbs)
=> Dict (ConcatListCtx2 as bs asbs (bs == asbs))
d :: Dict (ConcatListCtx2 as bs asbs (bs == asbs))
d = Dict
(as ~ as, Head as ~ Head as,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs))
-> Dict (ConcatListCtx2 as bs asbs (bs == asbs))
forall a b. a -> b
unsafeCoerce (Dict
(as ~ as, Head as ~ Head as,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs))
-> Dict (ConcatListCtx2 as bs asbs (bs == asbs)))
-> Dict
(as ~ as, Head as ~ Head as,
ConcatList (StripSuffix bs (Tail asbs)) bs (Concat (Tail as) bs))
-> Dict (ConcatListCtx2 as bs asbs (bs == asbs))
forall a b. (a -> b) -> a -> b
$ (as ~ as, Head as ~ Head as,
ConcatList (Tail as) bs (Tail asbs)) =>
Dict
(as ~ as, Head as ~ Head as, ConcatList (Tail as) bs (Tail asbs))
forall (a :: Constraint). a => Dict a
Dict
@(as ~ as, Head as ~ Head as, ConcatList (Tail as) bs (Tail asbs))
unsafeIncohBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])
. BareConstraint (SnocList as z bs)
unsafeIncohBareSnocList :: BareConstraint (SnocList as z bs)
unsafeIncohBareSnocList = BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
forall k (as :: [k]) (z :: k) (bs :: [k]).
BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
unsafeBareSnocList (BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs))
-> BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
forall a b. (a -> b) -> a -> b
$
BareConstraint (SnocList (Tail as) z (Tail bs))
-> BareConstraint (SnocListCtx as z bs)
forall k (as :: [k]) (z :: k) (bs :: [k]).
BareConstraint (SnocList (Tail as) z (Tail bs))
-> BareConstraint (SnocListCtx as z bs)
unsafeBareSnocListCtx @k @as @z @bs BareConstraint (SnocList (Tail as) z (Tail bs))
forall k (as :: [k]) (z :: k) (bs :: [k]).
BareConstraint (SnocList as z bs)
unsafeIncohBareSnocList
unsafeIncohBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList :: BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList = BareConstraint (ReverseList bs as)
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
forall k (as :: [k]) (bs :: [k]).
BareConstraint (ReverseList bs as)
-> BareConstraint (ReverseListCtx as bs)
-> BareConstraint (ReverseList as bs)
unsafeBareReverseList @k @as @bs
BareConstraint (ReverseList bs as)
forall k (as :: [k]) (bs :: [k]).
BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList
(BareConstraint (ReverseList (Tail as) (Init bs))
-> BareConstraint (ReverseListCtx as bs)
forall k (as :: [k]) (bs :: [k]).
BareConstraint (ReverseList (Tail as) (Init bs))
-> BareConstraint (ReverseListCtx as bs)
unsafeBareReverseListCtx @k @as @bs BareConstraint (ReverseList (Tail as) (Init bs))
forall k (as :: [k]) (bs :: [k]).
BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList)
unsafeIncohBareConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList :: BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList = BareConstraint (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatListCtx1 as bs asbs)
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
-> BareConstraint (ConcatList as bs asbs)
unsafeBareConcatList @k @as @bs @asbs
(BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
-> BareConstraint (ConcatListCtx1 as bs asbs)
unsafeBareConcatListCtx1 @k @as @bs @asbs BareConstraint (ConcatList (Tail as) bs (Tail asbs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList BareConstraint (ConcatList (Init as) (Last as : bs) asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList)
(BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList (Tail as) bs (Tail asbs))
-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
unsafeBareConcatListCtx2 @k @as @bs @asbs BareConstraint (ConcatList (Tail as) bs (Tail asbs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList)
{-# ANN nilInstSnocList (ToInstance NoOverlap) #-}
nilInstSnocList :: forall (k :: Type) (a :: k)
. Dict (SnocList '[] a '[a])
nilInstSnocList :: Dict (SnocList '[] a '[a])
nilInstSnocList
| Dict (ConcatList '[] '[a] '[a])
Dict <- Dict (ConcatList '[] '[a] '[a])
forall k (bs :: [k]). Dict (ConcatList '[] bs bs)
nilInstConcatList @k @'[a]
= ('[a] ~ Snoc '[] a, '[] ~ Init '[a], a ~ Last '[a],
SnocListCtx '[] a '[a], ConcatList '[] '[a] '[a]) =>
Dict (SnocList '[] a '[a])
forall k (as :: [k]) (a :: k) (bs :: [k]).
(bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs,
ConcatList as '[a] bs) =>
Dict (SnocList as a bs)
defineSnocList @k @'[] @a @'[a]
{-# ANN consInstSnocList (ToInstance NoOverlap) #-}
consInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) (a :: k) (b :: k)
. SnocList as z (b ': bs)
=> Dict (SnocList (a ': as) z (a ': b ': bs))
consInstSnocList :: Dict (SnocList (a : as) z (a : b : bs))
consInstSnocList
| Dict ((a : b : bs) ~ Snoc (a : as) z)
Dict <- Dict ((a : b : bs) ~ Snoc (a : as) z)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(a ': b ': bs) @(Snoc (a ': as) z)
, Dict ((a : as) ~ Init (a : b : bs))
Dict <- Dict ((a : as) ~ Init (a : b : bs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(a ': as) @(Init (a ': b ': bs))
, Dict (z ~ Last (a : b : bs))
Dict <- Dict (z ~ Last (a : b : bs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @z @(Last (a ': b ': bs))
, Dict (ConcatList (a : as) '[z] (a : b : bs))
Dict <- ConcatList as '[z] (b : bs) =>
Dict (ConcatList (a : as) '[z] (a : b : bs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]) (a :: k).
ConcatList as bs asbs =>
Dict (ConcatList (a : as) bs (a : asbs))
consInstConcatList @_ @as @'[z] @(b ': bs) @a
= ((a : b : bs) ~ Snoc (a : as) z, (a : as) ~ Init (a : b : bs),
z ~ Last (a : b : bs), SnocListCtx (a : as) z (a : b : bs),
ConcatList (a : as) '[z] (a : b : bs)) =>
Dict (SnocList (a : as) z (a : b : bs))
forall k (as :: [k]) (a :: k) (bs :: [k]).
(bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs,
ConcatList as '[a] bs) =>
Dict (SnocList as a bs)
defineSnocList @k @(a ': as) @z @(a ': b ': bs)
{-# ANN incohInstSnocList (ToInstance Incoherent) #-}
incohInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])
. bs ~ Snoc as z
=> Dict (SnocList as z bs)
incohInstSnocList :: Dict (SnocList as z bs)
incohInstSnocList = BareConstraint (SnocList as z bs) -> Dict (SnocList as z bs)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (SnocList as z bs) -> Dict (SnocList as z bs))
-> BareConstraint (SnocList as z bs) -> Dict (SnocList as z bs)
forall a b. (a -> b) -> a -> b
$ BareConstraint (SnocList as z bs)
forall k (as :: [k]) (z :: k) (bs :: [k]).
BareConstraint (SnocList as z bs)
unsafeIncohBareSnocList @k @as @z @bs
instance ReverseList ('[] :: [k]) ('[] :: [k])
{-# ANN consInstReverseList (ToInstance NoOverlap) #-}
consInstReverseList :: forall (k :: Type)
(a :: k) (as :: [k]) (b :: k) (bs :: [k])
. (ReverseList as (Init (b ': bs)), SnocList (Init (b ': bs)) a (b ': bs))
=> Dict (ReverseList (a ': as) (b ': bs))
consInstReverseList :: Dict (ReverseList (a : as) (b : bs))
consInstReverseList = BareConstraint (ReverseList (a : as) (b : bs))
-> Dict (ReverseList (a : as) (b : bs))
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict BareConstraint (ReverseList (a : as) (b : bs))
d
where
d :: BareConstraint (ReverseList (a : as) (b : bs))
d = (ReverseList (b : bs) (a : as)
=-> BareConstraint (ReverseList (a : as) (b : bs)))
-> BareConstraint (ReverseList (b : bs) (a : as))
-> BareConstraint (ReverseList (a : as) (b : bs))
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ReverseList (b : bs) (a : as)
=-> BareConstraint (ReverseList (a : as) (b : bs))
m (BareConstraint (ReverseList (a : as) (b : bs))
-> BareConstraint (ReverseList (b : bs) (a : as))
rev BareConstraint (ReverseList (a : as) (b : bs))
d)
m :: ReverseList (b ': bs) (a ': as)
=-> BareConstraint (ReverseList (a ': as) (b ': bs))
m :: ReverseList (b : bs) (a : as)
=-> BareConstraint (ReverseList (a : as) (b : bs))
m = (ReverseList (b : bs) (a : as) =>
BareConstraint (ReverseList (a : as) (b : bs)))
-> ReverseList (b : bs) (a : as)
=-> BareConstraint (ReverseList (a : as) (b : bs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic ReverseList (b : bs) (a : as) =>
BareConstraint (ReverseList (a : as) (b : bs))
f
f :: ReverseList (b ': bs) (a ': as)
=> BareConstraint (ReverseList (a ': as) (b ': bs))
f :: BareConstraint (ReverseList (a : as) (b : bs))
f | Dict ((a : as) ~ Reverse (b : bs))
Dict <- Dict ((a : as) ~ Reverse (b : bs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(a ': as) @(Reverse (b ': bs))
, Dict ((b : bs) ~ Reverse (a : as))
Dict <- Dict ((b : bs) ~ Reverse (a : as))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(b ': bs) @(Reverse (a ': as))
= Dict (ReverseList (a : as) (b : bs))
-> BareConstraint (ReverseList (a : as) (b : bs))
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (ReverseList (a : as) (b : bs))
forall k (as :: [k]) (bs :: [k]).
(as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as,
ReverseListCtx as bs) =>
Dict (ReverseList as bs)
defineReverseList
rev :: BareConstraint (ReverseList (a ': as) (b ': bs))
-> BareConstraint (ReverseList (b ': bs) (a ': as))
rev :: BareConstraint (ReverseList (a : as) (b : bs))
-> BareConstraint (ReverseList (b : bs) (a : as))
rev = BareConstraint (ReverseList (a : as) (b : bs))
-> BareConstraint (ReverseList (b : bs) (a : as))
forall a b. a -> b
unsafeCoerce
{-# ANN incohInstReverseList (ToInstance Incoherent) #-}
incohInstReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. bs ~ Reverse as
=> Dict (ReverseList as bs)
incohInstReverseList :: Dict (ReverseList as bs)
incohInstReverseList = BareConstraint (ReverseList as bs) -> Dict (ReverseList as bs)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ReverseList as bs) -> Dict (ReverseList as bs))
-> BareConstraint (ReverseList as bs) -> Dict (ReverseList as bs)
forall a b. (a -> b) -> a -> b
$ BareConstraint (ReverseList as bs)
forall k (as :: [k]) (bs :: [k]).
BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList @k @as @bs
{-# ANN incohInstConcatList (ToInstance Incoherent) #-}
incohInstConcatList :: forall (k :: Type) (as :: [k])
. Dict (ConcatList as ('[] :: [k]) as)
incohInstConcatList :: Dict (ConcatList as '[] as)
incohInstConcatList = BareConstraint (ConcatList as '[] as)
-> Dict (ConcatList as '[] as)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ConcatList as '[] as)
-> Dict (ConcatList as '[] as))
-> BareConstraint (ConcatList as '[] as)
-> Dict (ConcatList as '[] as)
forall a b. (a -> b) -> a -> b
$ BareConstraint (ConcatList as '[] as)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList @k @as @'[] @as
{-# ANN nilInstConcatList (ToInstance NoOverlap) #-}
nilInstConcatList :: forall (k :: Type) (bs :: [k])
. Dict (ConcatList '[] bs bs)
nilInstConcatList :: Dict (ConcatList '[] bs bs)
nilInstConcatList
| Dict ((bs == bs) ~ 'True)
Dict <- Dict ((bs == bs) ~ 'True)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(bs == bs) @'True
= (bs ~ Concat '[] bs, '[] ~ StripSuffix bs bs,
bs ~ StripPrefix '[] bs, ConcatListCtx1 '[] bs bs,
ConcatListCtx2 '[] bs bs (bs == bs)) =>
Dict (ConcatList '[] bs bs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
(asbs ~ Concat as bs, as ~ StripSuffix bs asbs,
bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs,
ConcatListCtx2 as bs asbs (bs == asbs)) =>
Dict (ConcatList as bs asbs)
defineConcatList @k @'[] @bs @bs
{-# ANN consInstConcatList (ToInstance NoOverlap) #-}
consInstConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) (a :: k)
. ConcatList as bs asbs
=> Dict (ConcatList (a ': as) bs (a ': asbs))
consInstConcatList :: Dict (ConcatList (a : as) bs (a : asbs))
consInstConcatList
| Dict ((bs == (a : asbs)) ~ 'False)
Dict <- Dict ((bs == (a : asbs)) ~ 'False)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(bs == (a ': asbs)) @'False
, Dict ((a : as) ~ StripSuffix bs (a : asbs))
Dict <- Dict ((a : as) ~ StripSuffix bs (a : asbs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(a ': as) @(StripSuffix bs (a ': asbs))
, Dict (bs ~ StripPrefix (a : as) (a : asbs))
Dict <- Dict (bs ~ StripPrefix (a : as) (a : asbs))
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @bs @(StripPrefix (a ': as) (a ': asbs))
, Dict ((a : asbs) ~ Concat (a : as) bs)
Dict <- Dict ((a : asbs) ~ Concat (a : as) bs)
forall k (a :: k) (b :: k). Dict (a ~ b)
unsafeEqTypes @(a ': asbs) @(Concat (a ': as) bs)
= let x :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=> Dict (ConcatList (a ': as) bs (a ': asbs))
x :: Dict (ConcatList (a : as) bs (a : asbs))
x = ((a : asbs) ~ Concat (a : as) bs,
(a : as) ~ StripSuffix bs (a : asbs),
bs ~ StripPrefix (a : as) (a : asbs),
ConcatListCtx1 (a : as) bs (a : asbs),
ConcatListCtx2 (a : as) bs (a : asbs) (bs == (a : asbs))) =>
Dict (ConcatList (a : as) bs (a : asbs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
(asbs ~ Concat as bs, as ~ StripSuffix bs asbs,
bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs,
ConcatListCtx2 as bs asbs (bs == asbs)) =>
Dict (ConcatList as bs asbs)
defineConcatList @k @(a ': as) @bs @(a ': asbs)
m :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=-> BareConstraint (ConcatList (a ': as) bs (a ': asbs))
m :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=-> BareConstraint (ConcatList (a : as) bs (a : asbs))
m = (ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs) =>
BareConstraint (ConcatList (a : as) bs (a : asbs)))
-> ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=-> BareConstraint (ConcatList (a : as) bs (a : asbs))
forall (c :: Constraint) r. (c => r) -> c =-> r
Magic (Dict (ConcatList (a : as) bs (a : asbs))
-> BareConstraint (ConcatList (a : as) bs (a : asbs))
forall (c :: Constraint). Dict c -> BareConstraint c
dictToBare Dict (ConcatList (a : as) bs (a : asbs))
ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs) =>
Dict (ConcatList (a : as) bs (a : asbs))
x)
shiftedCL :: BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
shiftedCL :: BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
shiftedCL = BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList
in BareConstraint (ConcatList (a : as) bs (a : asbs))
-> Dict (ConcatList (a : as) bs (a : asbs))
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ConcatList (a : as) bs (a : asbs))
-> Dict (ConcatList (a : as) bs (a : asbs)))
-> BareConstraint (ConcatList (a : as) bs (a : asbs))
-> Dict (ConcatList (a : as) bs (a : asbs))
forall a b. (a -> b) -> a -> b
$ (ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=-> BareConstraint (ConcatList (a : as) bs (a : asbs)))
-> BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
-> BareConstraint (ConcatList (a : as) bs (a : asbs))
forall (c :: Constraint) r. (c =-> r) -> BareConstraint c -> r
runMagic ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)
=-> BareConstraint (ConcatList (a : as) bs (a : asbs))
m BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
shiftedCL
inferConcat :: forall as bs asbs
. asbs ~ Concat as bs
=> Dict (ConcatList as bs asbs)
inferConcat :: Dict (ConcatList as bs asbs)
inferConcat = BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs))
-> BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall a b. (a -> b) -> a -> b
$ BareConstraint (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList @_ @as @bs @asbs
inferStripSuffix :: forall as bs asbs
. as ~ StripSuffix bs asbs
=> Dict (ConcatList as bs asbs)
inferStripSuffix :: Dict (ConcatList as bs asbs)
inferStripSuffix = BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs))
-> BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall a b. (a -> b) -> a -> b
$ BareConstraint (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList @_ @as @bs @asbs
inferStripPrefix :: forall as bs asbs
. bs ~ StripPrefix as asbs
=> Dict (ConcatList as bs asbs)
inferStripPrefix :: Dict (ConcatList as bs asbs)
inferStripPrefix = BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall (c :: Constraint). BareConstraint c -> Dict c
bareToDict (BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs))
-> BareConstraint (ConcatList as bs asbs)
-> Dict (ConcatList as bs asbs)
forall a b. (a -> b) -> a -> b
$ BareConstraint (ConcatList as bs asbs)
forall k (as :: [k]) (bs :: [k]) (asbs :: [k]).
BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList @_ @as @bs @asbs