Opened 14 months ago

Closed 14 months ago

Last modified 14 months ago

#15691 closed bug (invalid)

Marking Pred(S n) = n as injective

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.6.1
Keywords: TypeFamilies, InjectiveFamilies Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Should Pred be injective? Please close the ticket if this is a known limitation

{-# 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
  |  ^^^^^^^^^^^^^

Change History (2)

comment:1 Changed 14 months ago by monoidal

Cc: goldfire added
Resolution: invalid
Status: newclosed

Yes, it's a known limitation. See 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 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.

comment:2 Changed 14 months ago 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.

Note: See TracTickets for help on using tickets.