Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#5633 closed bug (invalid)

TypeFamilies don't seem to play with LIberalTypeSynonyms

Reported by: ocharles Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.0.4
Keywords: TypeFamilies LiberalTypeSynonyms Cc:
Operating System: Linux Architecture: x86
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

I'm trying to do some type level programming and want to use type families, but also LiberalTypeSynonyms to allow passing in a type level identity:

The following works:

{-# LANGUAGE LiberalTypeSynonyms #-}

type Id x = x

type Generic t (i:: * -> *) = i t

foo :: Generic Int Id
foo = undefined

However, replacing Generic with a type family does not work:

{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE TypeFamilies #-}

type Id x = x

type family Generic t (i:: * -> *)
type instance Generic Int i = i Int

foo :: Generic Int Id
foo = undefined

Hopefully I'm not over looking anything, but I can't see why this doesn't work.

Change History (2)

comment:1 Changed 4 years ago by simonpj

  • Resolution set to invalid
  • Status changed from new to closed

The first program works because of a non-Haskell98 feature of GHC. Fundamentally, type synonyms, and type families, must be fully applied. However with LiberalTypeSynonyms, GHC fully expands "outer" type synonyms before checking for the full application of "inner" ones. In this example, we start with

     foo : Generic Int Id

where Id is not fully applied. However, if Generic is a type synonym we expand it before making the check, so it's now like

     foo :: Id Int

and lo, Id is fully applies.

Now, type synonyms are easy to apply on the fly; it's another thing entirely with type families, which can "get stuck" (ie not reduce) if their arguments are no sufficiently informative Moreover, you can pattern match on their arguments. For example, if you wrote

	type instance Generic Int Maybe = Bool

would you expect that to work, with Maybe not matching against Id? Presumably not.

The pure type synonyms can always reduce, and never do pattern matching, so these issue do not arise. I can't see an easy way to lift the restriction.

comment:2 Changed 4 years ago by ocharles

Hi simon, thanks for the explanation.

It's a shame that it can't work, as a newtype doesn't really cut it. Fwiw, the motivation of this ticket came from trying to abstract away Record declarations in HaskellDB with code that also uses type families.

HaskellDB uses either RecCons FieldType (Expr RetType) or RecCons FieldType RetType depending on how a record is used/returned, and there doesn't seem to be a way to capture this with a type family, where I was trying to abstract Expr :: * -> * away. However, this ticket isn't the right place for that discussion, so I'll move that to a mailing list :)

Note: See TracTickets for help on using tickets.