Opened 3 years ago

Closed 23 months ago

Last modified 11 months ago

#12119 closed feature request (wontfix)

Can't create injective type family equation with TypeError as the RHS

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: CustomTypeErrors, TypeFamilies, InjectiveFamilies Cc: jstolarek, goldfire, Iceland_jack, sheaf
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

For the longest time, I've wanted to make a type family like this injective:

type family Foo (a :: *) :: * where
  Foo Bar = Int
  Foo Baz = Char

But the problem is that Foo is defined on all types of kind *, so the above definition is inherently non-injective. With the introduction of TypeErrors, however, I thought I could rule out all other cases:

import GHC.TypeLits

type family Foo (a :: *) = (r :: *) | r -> a where
  Foo Bar = Int
  Foo Baz = Char
  Foo _   = TypeError ('Text "boom")

But this doesn't work, sadly:

Injective.hs:18:3: error:                                                                 
    • Type family equations violate injectivity annotation:                               
        Foo Bar = Int -- Defined at Injective.hs:18:3                                     
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      Type variable ‘_’ cannot be inferred from the right-hand side.
      In the type family equation:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

From GHC's perspective, TypeError is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being TypeError is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that Foo a ~ Foo b (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that a ~ b.

Could this be accomplished by simply adding a special case for TypeError in the injectivity checker?

Change History (10)

comment:1 Changed 3 years ago by simonpj

That looks plausible to me.

What is the consequences of declaring Foo to be injective? Answer, only that if we have

 [W] g1 : Foo t1 ~ Foo t2

where [W] means "wanted", a constraint we are trying to solve, then we try to prove

 [W] g2: t1 ~ t2

Assuming we succeed, binding g2 = <some coercion>, then we can prove the first constraint by binding g1 = Foo g2.

If F is not injective, this proof strategy is no unsound; but it may be incomplete. Perhaps there are un-equal types t1 and t2 for which Foo t1 ~ Foo t2.

In your example, it's true that Foo Int ~ TypeError "boom" ~ Foo Bool. So indeed there may be a solution to the constraint Foo t1 ~ Foo t2 that does not require t1 ~ t2. But if the proof goes via TypeError, as here, perhaps that particular sort of incompleteness doesn't matter.

So it sounds plausible. I don't really know how to formalise it though.

comment:2 Changed 2 years ago by simonpj

Keywords: InjectiveFamilies added; Injective removed

comment:3 Changed 2 years ago by RyanGlScott

Note: this can be implemented in a dead-simple way:

  • compiler/typecheck/FamInst.hs

    diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
    index cabfb33..b56b68e 100644
    a b import VarSet 
    4242import Bag( Bag, unionBags, unitBag )
    4343import Control.Monad
    4444import NameEnv
     45import PrelNames
    4546import Data.List
    4647
    4748#include "HsVersions.h"
    makeInjectivityErrors fi_ax axiom inj conflicts 
    712713                               2 (vcat (map (pprCoAxBranch fi_ax) eqns))
    713714                          , coAxBranchSpan (head eqns) )
    714715        errorIf p f     = if p then [f err_builder axiom] else []
    715      in    errorIf are_conflicts  (conflictInjInstErr     conflicts     )
    716         ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
    717         ++ errorIf tf_headed       tfHeadedErr
    718         ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)
     716     in case rhs of
     717          TyConApp tc _
     718            | tyConName tc == errorMessageTypeErrorFamName -> []
     719          _ ->    errorIf are_conflicts  (conflictInjInstErr     conflicts     )
     720               ++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
     721               ++ errorIf tf_headed       tfHeadedErr
     722               ++ errorIf wrong_bare_rhs (bareVariableInRHSErr   bare_variables)

Of course, there's still Simon's point about formalizing this idea, which I have yet to do.

comment:4 Changed 2 years ago by simonpj

Of course, there's still Simon's point about formalizing this idea, which I have yet to do.

Yes: formalising it at least into a GHC propoosal would be good: it's a user-facing change.

comment:5 in reply to:  description Changed 23 months ago by RyanGlScott

Resolution: wontfix
Status: newclosed

It just occurred to me that the entire premise of this ticket is wrong. I claimed:

Replying to RyanGlScott:

For the longest time, I've wanted to make a type family like this injective:

type family Foo (a :: *) :: * where
  Foo Bar = Int
  Foo Baz = Char

But the problem is that Foo is defined on all types of kind *, so the above definition is inherently non-injective.

But the "inherently non-injective" part is totally bogus! In fact, as the code below demonstrates, Foo can be made injective quite easily:

{-# LANGUAGE TypeFamilyDependencies #-}

data Bar
data Baz

type family Foo (a :: *) = (r :: *) | r -> a where
  Foo Bar = Int
  Foo Baz = Char

I don't know why I believed that crazy misconception about injectivity vis-à-vis exhaustivity, but in any case, the entire reason why I was pursuing this feature in the first place has vanished. In light of this, I don't think it's worth adding this much extra complexity to the type family injectivity checker.

comment:6 Changed 11 months ago by sheaf

What about the following:

data Dim
  = D2
  | D3
  | D4

type family ToDim (n :: Nat) = d | d -> n where
  ToDim 2 = D2
  ToDim 3 = D3
  ToDim 4 = D4
  ToDim n = TypeError 
    ( Text "Error: dimension must be 2, 3 or 4 (given: "
     :<>: ShowType n :<>: Text ")" )

This seems useful to me, as it allows one to switch easily between two different representations of dimension (which have different uses: with Nats I can do arithmetic, but the explicit enum is more convenient with singletons for instance).

I feel like the injectivity annotation should be allowed in this case (but I am not aware of any of the theory which backs injective type families).

comment:7 Changed 11 months ago by Iceland_jack

Cc: Iceland_jack added

comment:8 in reply to:  6 Changed 11 months ago by AntC

Replying to sheaf:

What about the following: ...

This seems useful to me, ...

Sure, it's the same structure as the O.P.

I feel like the injectivity annotation should be allowed in this case ...

It is. Ryan's comment:5 says what's not allowed is the TypeError catch-all equation -- that is, if you want ToDim to be injective.

So if you call ToDim 5, inference will get stuck, and you'll get an error message somewhere/somehow else.

comment:9 Changed 11 months ago by sheaf

Cc: sheaf added

I understand that the type family is injective if I remove the type error.
However I would prefer a custom error message, as opposed to the user getting some confusing error about a stuck type family application. In my opinion, one of the advantages of injectivity annotation is that internal use of the type family doesn't end up leaking into the front-end.

Last edited 11 months ago by sheaf (previous) (diff)

comment:10 Changed 11 months ago by AntC

The injectivity annotation is a promise that all your equations are injective.

Then consider the return type of ToDim 5 compared to ToDim 6 (if you put a TypeError equation): they're the same type. Then that equation is not injective.

Specifically, ShowType n is not injective: it's an existentially-quantified data constructor, promoted to a datakind.

If you omit the TypeError equation, there's an implicit ToDim n = ToDim n added at the end. That is injective.

Possibly you could put some other error-handling logic, that preserves plain n on the rhs, then that would be injective.

Note: See TracTickets for help on using tickets.