#15691: Marking Pred(S n) = n as injective
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.6.1
(Type checker) |
Keywords: TypeFamilies, | Operating System: Unknown/Multiple
InjectiveFamilies |
Architecture: | Type of failure: None/Unknown
Unknown/Multiple |
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
Should `Pred` be injective? Please close the ticket if this is a known
limitation
{{{#!hs
{-# Language DataKinds, TypeFamilyDependencies #-}
data N = O | S N
type family
Pred n = res | res -> n where
Pred(S n) = n
}}}
fails with
{{{
• Type family equation violates injectivity annotation.
RHS of injective type family equation is a bare type variable
but these LHS type and kind patterns are not bare variables: ‘'S n’
Pred ('S n) = n -- Defined at 462.hs:7:2
• In the equations for closed type family ‘Pred’
In the type family declaration for ‘Pred’
|
7 | Pred(S n) = n
| ^^^^^^^^^^^^^
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15691>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
