Pattern synonyms work where constructors fail
This may be a bug.
Taken from reddit thread:
{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, MultiParamTypeClasses,
PatternSynonyms, TupleSections, TypeFamilies,
TypeFamilyDependencies, TypeOperators, ViewPatterns #-}
-- ...
type family Sum (ts :: [*]) = (t :: *) | t -> ts where
Sum (t ': ts) = Either t (Sum ts)
Sum '[] = Void
pattern At :: (KnownNatural n, Index n ts) => SNatural n -> (ts !! n) -> Sum ts
pattern At sn t <- (at -> Just (sn, t)) where At = toSum
at :: (KnownNatural n, Index n ts) => Sum ts -> Maybe (SNatural n, ts !! n)
at = fmap (sn,) . ofSum sn where sn = knownNatural
class Index (n :: Natural) (ts :: [*]) where
type (!!) ts n :: *
toSum :: SNatural n -> (ts !! n) -> Sum ts
ofSum :: SNatural n -> Sum ts -> Maybe (ts !! n)
instance Index n ts => Index ('Succ n) (t ': ts) where
type (!!) (t ': ts) ('Succ n) = ts !! n
toSum (SSucc sn) = Right . toSum sn
ofSum (SSucc sn) = either (const Nothing) (ofSum sn)
instance Index 'Zero (t ': ts) where
type (!!) (t ': ts) 'Zero = t
toSum SZero = Left
ofSum SZero = either Just (const Nothing)
data Natural = Zero | Succ Natural
data SNatural (n :: Natural) where
SZero :: SNatural 'Zero
SSucc :: SNatural n -> SNatural ('Succ n)
class KnownNatural (n :: Natural) where
knownNatural :: SNatural n
instance KnownNatural 'Zero where
knownNatural = SZero
instance KnownNatural n => KnownNatural ('Succ n) where
knownNatural = SSucc knownNatural
Using SZero
, SSucc SZero
, ... fails
type Trit = Sum '[(), (), ()]
fromTrit :: Trit -> Int
fromTrit (At SZero ()) = 0
fromTrit (At (SSucc SZero) ()) = 1
fromTrit (At (SSucc (SSucc SZero)) ()) = 2
but making pattern synonyms succeeds
pattern S0 :: SNatural 'Zero
pattern S0 = SZero
pattern S1 :: SNatural ('Succ 'Zero)
pattern S1 = SSucc S0
pattern S2 :: SNatural ('Succ ('Succ 'Zero))
pattern S2 = SSucc S1
type Trit = Sum '[(), (), ()]
fromTrit :: Trit -> Int
fromTrit (At S0 ()) = 0
fromTrit (At S1 ()) = 1
fromTrit (At S2 ()) = 2
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |