[GHC] #15691: Marking Pred(S n) = n as injective
#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
#15691: Marking Pred(S n) = n as injective -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Keywords: TypeFamilies, Resolution: invalid | InjectiveFamilies 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 monoidal): * status: new => closed * cc: goldfire (added) * resolution: => invalid Comment: Yes, it's a known limitation. See [http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton- jones_eisenberg_injectivity.pdf "Injective Type Families for Haskell"], section 4.1, "Awkward Case 2". By definition of `Pred` we have `Pred (S (Pred Zero)) ~ Pred Zero`. If `Pred` is recognized as injective, then `Zero ~ S (Pred Zero)`, which is a contradiction. The problem is that `Pred Zero` is a valid type, even though it's outside of the domain of `Pred`. See also #9636. The [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1075&context=compsci_pubs Constrained Type Families] paper resolves this by representing the domain of the type function as a constraint. I don't know if there are plans to implement it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15691#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15691: Marking Pred(S n) = n as injective -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1 checker) | Keywords: TypeFamilies, Resolution: invalid | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): There are no current plans to implement "Constrained Type Families". The natural way to do it requires dependent types (because it requires the appearance of dictionaries, which are terms, in types). We could hack something together that didn't use dependent types, but it would be a hack. I would love to see Constrained Type Families indeed implemented once we have dependent types. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15691#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC