[GHC] #14104: Pattern synonyms work where constructors fail
#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
#14104: Pattern synonyms work where constructors fail -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: This is behaving as expected. The types of the constructor `SZero` and the pattern synonym `S0` are almost the same, but not quite. You'll notice that if you leave off the type signature for `S0`, then `fromTrit` will fail to compile: {{{ Bug.hs:58:11: error: • Ambiguous type variable ‘n0’ arising from a pattern prevents the constraint ‘(KnownNatural n0)’ from being solved. Probable fix: use a type annotation to specify what ‘n0’ should be. These potential instances exist: instance KnownNatural n => KnownNatural ('Succ n) -- Defined at Bug.hs:42:10 instance KnownNatural 'Zero -- Defined at Bug.hs:40:10 • In the pattern: At S0 () In an equation for ‘fromTrit’: fromTrit (At S0 ()) = 0 | 58 | fromTrit (At S0 ()) = 0 | ^^^^^^^^ }}} Which is the same error you'd get if you tried using `SZero` in place of `S0` in the definition of `fromTrit`. The reason is that while the (written) type signature of `S0` is `SNatural 'Zero`, if you let GHC infer what it should be, then you'll get: {{{ λ> :i S0 pattern S0 :: () => n ~ 'Zero => SNatural n -- Defined at Bug.hs:47:1 }}} That is, `S0`'s inferred type is `SNatural n`, under the //given constraint// that `n` is equal to `Zero`. That is to say, in the context of a pattern match, we can only assume this equality //after// we've matched on it. This is why `fromTrit` is failing to typecheck with the constructor `SZero` (or `S0` with an inferred type), since we need evidence that `n ~ Zero` when matching on `At` (which comes before `SZero`/`S0`). To work around this issue, one can simply use the original pattern synonym type signatures, or one can try the workarounds that Syrak lists in this [https://www.reddit.com/r/haskell/comments/6so95h/why_do_pattern_synonyms_wor... helpful comment]. Really, all of this is a symptom of the way typechecking GADT patterns works. Intuitively, one might expect that GHC gathers all of the given constraints in every pattern of a clause before typechecking each pattern, but that's not how it works. In practice, GHC typechecks patterns in a [https://ghc.haskell.org/trac/ghc/ticket/12018 left-to-right, inside-out fashion]. This is compositional and works predictably, but is has the downside that there some sequences of patterns that will only typecheck if ordered in a certain way (and alas, `At SZero` is not ordered the right way). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14104#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC