{-# 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 = 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 = 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 = defineConcatList
unsafeBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])
. BareConstraint (SnocListCtx as z bs)
-> BareConstraint (SnocList as z bs)
unsafeBareSnocList = runMagic m
where
m :: SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)
m | Dict <- unsafeEqTypes @bs @(Snoc as z)
, Dict <- unsafeEqTypes @as @(Init bs)
, Dict <- unsafeEqTypes @z @(Last bs)
, Dict <- unsafeEqTypes @bs @(Concat as '[z])
, Dict <- inferConcat @as @'[z] @bs
= Magic (dictToBare $ 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 = runMagic . runMagic m
where
m :: ReverseList bs as
=-> ReverseListCtx as bs
=-> BareConstraint (ReverseList as bs)
m | Dict <- unsafeEqTypes @as @(Reverse bs)
, Dict <- unsafeEqTypes @bs @(Reverse as)
= Magic (Magic (dictToBare $ 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 = runMagic . runMagic m
where
m :: ConcatListCtx1 as bs asbs
=-> ConcatListCtx2 as bs asbs (bs == asbs)
=-> BareConstraint (ConcatList as bs asbs)
m | Dict <- unsafeEqTypes @as @(StripSuffix bs asbs)
, Dict <- unsafeEqTypes @bs @(StripPrefix as asbs)
, Dict <- unsafeEqTypes @asbs @(Concat as bs)
= Magic (Magic (dictToBare $ 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 = runMagic m
where
m :: SnocList (Tail as) z (Tail bs) =-> BareConstraint (SnocListCtx as z bs)
m = Magic (dictToBare d)
d :: SnocList (Tail as) z (Tail bs) => Dict (SnocListCtx as z bs)
d = unsafeCoerce $ 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
= runMagic (runMagic m unsafeIncohBareSnocList)
where
m :: SnocList (Init bs) (Head as) bs
=-> ReverseList (Tail as) (Init bs)
=-> BareConstraint (ReverseListCtx as bs)
m = Magic (Magic (dictToBare f))
f :: ( SnocList (Init bs) (Last bs) bs
, ReverseList (Tail as) (Init bs)
)
=> Dict (ReverseListCtx as bs)
f | Dict <- unsafeEqTypes @(Head as) @(Last bs)
= unsafeCoerce (
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 = runMagic . runMagic m
where
m :: ConcatList (Tail as) bs (Tail asbs)
=-> ConcatList (Init as) (Last as ': bs) asbs
=-> BareConstraint (ConcatListCtx1 as bs asbs)
m = Magic (Magic (dictToBare d))
d :: ( ConcatList (Tail as) bs (Tail asbs)
, ConcatList (Init as) (Last as ': bs) asbs)
=> Dict (ConcatListCtx1 as bs asbs)
d = unsafeCoerce $ 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 = runMagic m
where
m :: ConcatList (Tail as) bs (Tail asbs)
=-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))
m = Magic (dictToBare d)
d :: ConcatList (Tail as) bs (Tail asbs)
=> Dict (ConcatListCtx2 as bs asbs (bs == asbs))
d = unsafeCoerce $ 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 = unsafeBareSnocList $
unsafeBareSnocListCtx @k @as @z @bs unsafeIncohBareSnocList
unsafeIncohBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. BareConstraint (ReverseList as bs)
unsafeIncohBareReverseList = unsafeBareReverseList @k @as @bs
unsafeIncohBareReverseList
(unsafeBareReverseListCtx @k @as @bs unsafeIncohBareReverseList)
unsafeIncohBareConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])
. BareConstraint (ConcatList as bs asbs)
unsafeIncohBareConcatList = unsafeBareConcatList @k @as @bs @asbs
(unsafeBareConcatListCtx1 @k @as @bs @asbs unsafeIncohBareConcatList unsafeIncohBareConcatList)
(unsafeBareConcatListCtx2 @k @as @bs @asbs unsafeIncohBareConcatList)
{-# ANN nilInstSnocList (ToInstance NoOverlap) #-}
nilInstSnocList :: forall (k :: Type) (a :: k)
. Dict (SnocList '[] a '[a])
nilInstSnocList
| Dict <- nilInstConcatList @k @'[a]
= 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 <- unsafeEqTypes @(a ': b ': bs) @(Snoc (a ': as) z)
, Dict <- unsafeEqTypes @(a ': as) @(Init (a ': b ': bs))
, Dict <- unsafeEqTypes @z @(Last (a ': b ': bs))
, Dict <- consInstConcatList @_ @as @'[z] @(b ': bs) @a
= 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 = bareToDict $ 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 = bareToDict d
where
d = runMagic m (rev d)
m :: ReverseList (b ': bs) (a ': as)
=-> BareConstraint (ReverseList (a ': as) (b ': bs))
m = Magic f
f :: ReverseList (b ': bs) (a ': as)
=> BareConstraint (ReverseList (a ': as) (b ': bs))
f | Dict <- unsafeEqTypes @(a ': as) @(Reverse (b ': bs))
, Dict <- unsafeEqTypes @(b ': bs) @(Reverse (a ': as))
= dictToBare $ defineReverseList
rev :: BareConstraint (ReverseList (a ': as) (b ': bs))
-> BareConstraint (ReverseList (b ': bs) (a ': as))
rev = unsafeCoerce
{-# ANN incohInstReverseList (ToInstance Incoherent) #-}
incohInstReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])
. bs ~ Reverse as
=> Dict (ReverseList as bs)
incohInstReverseList = bareToDict $ unsafeIncohBareReverseList @k @as @bs
{-# ANN incohInstConcatList (ToInstance Incoherent) #-}
incohInstConcatList :: forall (k :: Type) (as :: [k])
. Dict (ConcatList as ('[] :: [k]) as)
incohInstConcatList = bareToDict $ unsafeIncohBareConcatList @k @as @'[] @as
{-# ANN nilInstConcatList (ToInstance NoOverlap) #-}
nilInstConcatList :: forall (k :: Type) (bs :: [k])
. Dict (ConcatList '[] bs bs)
nilInstConcatList
| Dict <- unsafeEqTypes @(bs == bs) @'True
= 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 <- unsafeEqTypes @(bs == (a ': asbs)) @'False
, Dict <- unsafeEqTypes @(a ': as) @(StripSuffix bs (a ': asbs))
, Dict <- unsafeEqTypes @bs @(StripPrefix (a ': as) (a ': asbs))
, Dict <- 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 = 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 = Magic (dictToBare x)
shiftedCL :: BareConstraint
(ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))
shiftedCL = unsafeIncohBareConcatList
in bareToDict $ runMagic m shiftedCL
inferConcat :: forall as bs asbs
. asbs ~ Concat as bs
=> Dict (ConcatList as bs asbs)
inferConcat = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs
inferStripSuffix :: forall as bs asbs
. as ~ StripSuffix bs asbs
=> Dict (ConcatList as bs asbs)
inferStripSuffix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs
inferStripPrefix :: forall as bs asbs
. bs ~ StripPrefix as asbs
=> Dict (ConcatList as bs asbs)
inferStripPrefix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs