[GHC] #14104: Pattern synonyms work where constructors fail

10 Aug 2017

      #14104: Pattern synonyms work where constructors fail
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This may be a bug.

 Taken from
 [https://www.reddit.com/r/haskell/comments/6so95h/why_do_pattern_synonyms_wor...
 reddit thread]:

 {{{#!hs
 {-# 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

 {{{#!hs
 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

 {{{#!hs
 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
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14104
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler