:kind! accepts unsaturated type aliases

Here's a ghci session:

> :set -XTypeFamilies -XPolyKinds
> type family Id (a :: k)
> type instance Id a = a
> type Foo x = Maybe
> :kind! Id Foo
Id Foo :: *
= Id Foo

I think the final :kind! query should throw an error instead, complaining that Foo hasn't been given enough arguments. (But even if you disagree, and think it should be allowed, * is clearly not the right kind!)

Using a normal type alias in place of the type family for Id also allows the query incorrectly, though it does at least report a sensible kind.

Although I think it shouldn't matter, I have checked with -ignore-dot-ghci to make sure I haven't accidentally turned LiberalTypeSynonyms on.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #13962 (closed)

changed milestone to %8.6.3

changed weight to 5

added Tbug Trac import labels

Okay, so further thinking, I'd like to retract part of the complaint. I believe I understand why it decides on kind *, and agree that's a sensible answer. (Namely: I thought in my head Id :: k -> k, but the compiler chose Id :: k -> *, following exactly the rules set out in the documentation, so the compiler was right and I was wrong. And I thought in my head Id a = a matches all types so Id Foo should reduce to Foo if it works at all, but the compiler thought Id a = a only matches when a :: *, so Id Foo is a stuck term not one that can reduce, and again the compiler was right and I was wrong.)

But I still think it should probably complain about applying a type family or type alias to an unsaturated type alias.

:kind deliberately allows unsaturated uses of type synonyms and type families—see this section of the users' guide. Many folks find it quite handy to be able to query the kinds of type synonyms with :kind (e.g., :kind Id), but disallowing unsaturated type synonyms/families //carte blanche// would prevent :kind Id from working, so a special case was added to allow it in that particular scenario.

(Also note that this has been previously discussed in #13962 (closed).)

Trac metadata

Trac field	Value
Related	- → #13962 (closed)

Sure, I understand the motivation.

It seems like a sensible middle ground would be to special-case only top-level unsaturated type aliases/families, and not wholesale allow unsaturation. And indeed the way the documentation was written makes it sound like that's the case: it uses the precise language ":kind even allows you to write a partial application of a type synonym", whereas Id Foo is not a partial application of a type synonym but rather the application of a type (family) to a partial application of a type synonym.

Replying to [ticket:16013#comment:164839 dmwit]:

whereas Id Foo is not a partial application of a type synonym but rather the application of a type (family) to a partial application of a type synonym.

Indeed. Still, removing this feature would be a breaking change (albeit a slight one), so that's something to consider. It might be worth opening a GHC proposal about this.

My own vote is that we drop the saturation requirement only at top-level, calling the current implementation a bug. To my horror, GHC allows this interaction:

type family Map f x where
  Map _ '[] = '[]
  Map f (x : xs) = f x : Map f xs

data Nat = Zero | Succ Nat

type family Pred n where
  Pred Zero = Zero
  Pred (Succ n) = n

λ> :kind! Map Pred [Succ (Succ Zero), Succ (Succ (Succ Zero)), Zero]
Map Pred [Succ (Succ Zero), Succ (Succ (Succ Zero)), Zero] :: [Nat]
= '[ 'Succ 'Zero, 'Succ ('Succ 'Zero), 'Zero]

Ticket retargeted after milestone closed

mentioned in issue #16068 (closed)

My own vote is that we drop the saturation requirement only at top-level, calling the current implementation a bug.

I'm fine with this. Ryan, might you execute on this? Thanks!

Are we OK with pushing through a breaking change without an accompanying GHC proposal?

I'm OK with that. This is a bug, and this ticket proposes a fix. I don't think a proposal is needed.

Alright, then here's a patch.

Trac metadata

Trac field	Value
Differential revisions	- → D5471

mentioned in commit 6b70cf61

closed

changed milestone to %8.8.1

Landed in 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

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → ghci/should_fail/T16013

added Pnormal label