Opened 3 years ago

Last modified 13 months ago

#8828 new feature request

Type pattern synonyms

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


Hi, it would be nice if the following example were acceptable:

{-# LANGUAGE FlexibleInstances, TypeFamilies, TypeSynonymInstances #-}
data X a = X a
type family TX a
type instance TX a = X a

instance Show (TX Int)

But ghc complains that it cannot substitute the instance of TX:

    Illegal type synonym family application in instance: TX Int
    In the instance declaration for ‛Show (TX Int)’

A more practical (but not self-contained) example involving extensible records looks

Change History (5)

comment:1 Changed 3 years ago by simonpj

Owner: set to goldfire

Initially this seems very reasonable. The rule would be this: you normalise the instance type, and check that there are no remaining type family calls. (Currently we check that there are no type-family calls at all.)

After all, with -XFlexibleInstances you can use type synonyms in instance heads (manual entry), and this ticket is just an extension of the same idea.

But it's not entirely straightforward. For uniformity you'll also have to allow type-family applications in type-family instances too:

type instance F (TX Int) = Bool
data instance D (TX Int) = D1 | D2

Now does this impose a dependency order among family instances?

type instance F (F Int) = Bool
type instance F Int = Char

and what if it were type instance F Int = Int? Maybe we could disallow that, by disallowing "recursion on the left".

Or what about

class D a where
  type F a

instance C (F Int) where ...

instance D Int where
  type F Int = Bool

Now perhaps we have to process the second instance declaration before the first?

Richard will work on this in due course.


Last edited 3 years ago by simonpj (previous) (diff)

comment:2 Changed 3 years ago by goldfire

I've thought about this ticket some, and I think implementing this idea is a move in the wrong direction.

Implementing this idea feels quite like allowing function applications in patterns. For example, how would we feel about this:

foo :: Bool -> Int
foo True = 1
foo (not True) = -1

With some engineering, there is no reason that we couldn't accept a definition such as the one above. After all, not True is fully applied to constants and can be reduced to False. We can pretend that there is a TH-like stage restriction (somewhat like Simon's quite valid dependency concerns in comment:1) to prevent infinite regress. We can even check to make sure that the pattern match is complete. Yet, this definition smells like rotten eggs to me.

Should it be different at the type level? I, personally, think not.

What it seems we really want here are type pattern synonyms. Pattern synonyms allow a richer syntax "on the left of an =", which is what we want here in types. It so happens that, currently, type patterns are syntactically just types that don't mention type families, but if we separate out a type pattern syntax from a type syntax (which I think is a good idea -- they are different!) then the idea of type families "on the left" becomes even more suspicious and type pattern synonyms make more sense.

So, instead of implementing the idea proposed here, I would rather think about type pattern synonyms. How are these related to term pattern synonyms? How would we declare them? Can they be promoted to kinds? etc.

What do others think here?

comment:3 Changed 3 years ago by simonpj

I rather agree with Richard here.


comment:4 Changed 2 years ago by goldfire

difficulty: UnknownProject (more than a week)
Owner: goldfire deleted
Summary: allow fully applied type families in instance headsType pattern synonyms

According to the discussion above, this is really a new feature that needs to be designed and implemented. I'm releasing ownership, though I can conceive of a future where I take this on again.

comment:5 Changed 13 months ago by thomie

Component: CompilerCompiler (Type checker)
Note: See TracTickets for help on using tickets.