Opened 2 years ago

Closed 2 years ago

Last modified 8 months ago

#13962 closed bug (wontfix)

GHCi allows unsaturated type family

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

Description (last modified by Iceland_jack)

Taken from Promoting Functions to Type Families in Haskell

{-# Language TypeFamilies, PolyKinds, DataKinds, TypeOperators #-}

type family
  Map (f :: a -> b) (xs :: [a]) :: [b] where
  Map f '[]       = '[]
  Map f (x ': xs) = f x ': Map f xs

data N = O | S N

type family
  Pred (n :: N) :: N where
  Pred O     = O
  Pred (S n) = n

-- The type family ‘Map’ should have 2 arguments, but has been given 1
type MapPred = Map Pred

fails as expected, but commenting it out and writing Map Pred works in GHCi

ghci> :kind Map Pred
Map Pred :: [N] -> [N]
ghci> :kind! Map Pred '[S (S O), S O, O]
Map Pred '[S (S O), S O, O] :: [N]
= '['S 'O, 'O, 'O]

I can only test this in GHC 7.8, 8 now. I know GHCi has weird rules for unsaturated type families but I figured I'd write a ticket because the slides say "But it is invalid to write: Map Pred '[O, S O]".

Change History (7)

comment:1 Changed 2 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott goldfire added
Keywords: TypeFamilies added

Wow, that's astounding that it actually gives you the right answer...

Richard, do you know how this is even working? Because I have to admit, this is shaking my faith in the belief that we need defunctionalization to partially apply type families ;)

comment:3 Changed 2 years ago by goldfire

GHC is behaving according to its manual. See this section.

We made a special case for :kind some years ago to allow queries like :kind Map. The user sensibly wants Map's kind, and we should give it to them. So the TF-saturation requirement is dropped in :kind. I support this design choice.

On the other hand, it's very suspect in :kind!. It's surprising to me, too, that this gives the right result. But, after all, TF evaluation makes fine sense with unsaturated type families -- it's just type inference that gets muddled. So: we could keep the current behavior (which doesn't seem to be hurting anyone), or restrict the behavior of kind! to disallow partially applied type families. Maybe an intermediate approach is to keep the current behavior but issue a warning in the event of a partially applied family.

comment:4 Changed 2 years ago by RyanGlScott

I see. I'm a bit embarrassed that I've been doing :kind Map all this time and never realized that I was doing something unsavory.

I'm curious - how does type inference get muddled exactly? And moreover, is the particular way in which it becomes muddled relevant for :kind? If not, then I'd vote to leave things the way they are. Otherwise, we might want to reconsider.

comment:5 Changed 2 years ago by goldfire

The muddiness all comes down to this: If GHC knows m a ~ Maybe Int, should it choose m ~ Maybe and a ~ Int? After all, if m could be an unsaturated type family, committing to the above decomposition would be wrong.

This kind of inference seems unlikely in :kind or :kind!, though I can't rule it out if someone tried to.

In the end, I think we should just keep the current behavior.

comment:6 in reply to:  5 Changed 2 years ago by RyanGlScott

Resolution: wontfix
Status: newclosed

Replying to goldfire:

The muddiness all comes down to this: If GHC knows m a ~ Maybe Int, should it choose m ~ Maybe and a ~ Int? After all, if m could be an unsaturated type family, committing to the above decomposition would be wrong.

This kind of inference seems unlikely in :kind or :kind!, though I can't rule it out if someone tried to.

Thanks for explaining this.

In the end, I think we should just keep the current behavior.

That sounds reasonable to me. Given that there's already a section in the users' manual about this, I'd say we can just close this ticket.

comment:7 Changed 8 months ago by RyanGlScott

Note that we opted to disallow unsaturated type synonyms/families in GHCi when not at the top level in commit 6b70cf611e5ddc475edaa54b893d20990699ddb8:

commit 6b70cf611e5ddc475edaa54b893d20990699ddb8
Author: Ryan Scott <ryan.gl.scott@gmail.com>
Date:   Tue Jan 8 07:37:18 2019 -0500

    Be pickier about unsaturated synonyms in :kind
    
    Summary:
    We currently permit any and all uses of unsaturated type
    synonyms and type families in GHCi's `:kind` command, which allows
    strange interactions like this one:
    
    ```
    > :set -XTypeFamilies -XPolyKinds
    > type family Id (a :: k)
    > type instance Id a = a
    > type Foo x = Maybe
    > :kind! Id Foo
    ```
    
    This is probably a stretch too far, so this patch moves to disallow
    unsaturated synonyms that aren't at the top level (we still want to
    allow `:kind Id`, for instance). We do this by augmenting `GhciCtxt`
    with an additional `Bool` field to indicate if we are at the
    outermost level of the type being passed to `:kind` or not. See
    `Note [Unsaturated type synonyms in GHCi]` in `TcValidity` for the
    full story.
    
    Test Plan: make test TEST=T16013
    
    Reviewers: goldfire, bgamari
    
    Reviewed By: goldfire
    
    Subscribers: simonpj, goldfire, rwbarton, carter
    
    GHC Trac Issues: #16013
    
    Differential Revision: https://phabricator.haskell.org/D5471

See #16013.

Note: See TracTickets for help on using tickets.