Opened 4 years ago

Last modified 6 days ago

#9269 new feature request

Type families returning quantified types

Reported by: pumpkin Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.2
Keywords: TypeFamilies Cc: RyanGlScott, Iceland_jack, int-index, glaebhoerl
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking: #11962
Related Tickets: #13901 Differential Rev(s):
Wiki Page:

Description

Is there a fundamental reason for not being able to use quantification in a type family? I'd very much like to be able to do it, obviously turning on RankNTypes if necessary.

I'm looking for things like this:

type family Foo (x :: Bool) where
  Foo True = forall a. [a]
  Foo False = ()

Change History (8)

comment:1 Changed 4 years ago by goldfire

It depends on how "fundamental" a reason you want.

Consider this:

type family Foo (x :: Bool) where
  Foo True = forall a. a -> a -> a
  Foo False = ()

data SBool :: Bool -> * where
  STrue :: SBool True
  SFalse :: SBool False

bar :: SBool b -> Foo b -> ()
bar STrue x = (x 'a' 'b', x True False) `seq` ()
bar SFalse x = x

It seems to be that it would be reasonable to expect the above code to typecheck, if we're allowed to write a family Foo. But, getting this to work wreaks havoc with the way GHC's typechecker is built.

GHC walks over a term and builds up a set of constraints. For example, if the term is something like z True, then GHC will decide that z has type alpha, for some unknown type alpha. Then, it says that we must have alpha ~ (beta -> gamma), from the fact that z is in a function position. We then see that beta ~ Bool from the type of True. After walking over an entire term, GHC then solves these constraints, in this case getting that the type of z must be (Bool -> gamma).

The crucial problem in the code above is that this algorithm runs into trouble on the RHS of the first clause of bar. GHC will see that x is used in a function position and will try to infer a type like alpha -> beta for x, which is dead wrong. "But wait," you say: "GHC can know that x should have type forall a. a -> a -> a by then!" Well, not quite. GHC knows that x has type Foo b (from the type signature) and that b ~ True (from the GADT pattern-match), but it hasn't yet put those pieces together: that's what the solver does! And, we don't want to try to run the solver before generating all the constraints, because the solver might do the wrong thing when it doesn't have enough information.

One possible way forward here is to modify the offending line of the program above as follows:

bar STrue (x :: forall a. a -> a -> a) = ...

Now, GHC knows the correct type of x on the RHS and can generate constraints there without a problem. When the solver runs, it needs to solve Foo b ~ forall a. a -> a -> a, which works out just fine, given the GADT pattern-match.

This requirement (the extra type annotation) is strange and unexpected to users, who are likely not thinking about GHC's constraint-solving algorithm. Does this fact make your proposed feature a bad idea? I don't know. And, there may be yet other reasons why what you want is a bad idea; this one is just one possible reason.

Do others know of other problems here?

comment:3 Changed 2 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:4 Changed 2 years ago by thomie

Keywords: TypeFamilies added

comment:5 Changed 5 months ago by RyanGlScott

Blocking: 11962 added
Cc: RyanGlScott added

comment:6 Changed 5 months ago by Iceland_jack

Cc: Iceland_jack added

comment:7 Changed 5 months ago by int-index

Cc: int-index added

comment:8 Changed 6 days ago by glaebhoerl

Cc: glaebhoerl added
Note: See TracTickets for help on using tickets.