GHC doesn't think a type is of kind *, despite having evidence for it

[RyanGlScott]

The easiest way to illustrate this bug is this:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

import Data.Kind (Type)

blah :: forall (a :: k). k ~ Type => a -> a
blah x = x

$ ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Foo.hs, interpreted )

Foo.hs:8:43: error:
    • Expected a type, but ‘a’ has kind ‘k’
    • In the type signature:
        blah :: forall (a :: k). k ~ Type => a -> a

I find this behavior quite surprising, especially since we have evidence that k ~ Type in scope!

If the program above looks too contrived, consider a similar program that uses Typeable. I want to write something like this:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind (Type)
import Data.Typeable

foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
    => proxy a -> String
foo _ =
  case eqT :: Maybe (k :~: Type) of
    Nothing   -> "Non-Type kind"
    Just Refl ->
      case eqT :: Maybe (a :~: Int) of
        Nothing   -> "Non-Int type"
        Just Refl -> "It's an Int!"

This exhibits the same problem. Despite the fact that we pattern-matched on a Refl of type k :~: Type, GHC refuses to consider the possibility that a :~: Int is well kinded, even though (a :: k), and we learned from the first Refl that k ~ Type!

[goldfire]

For your first example: this infelicity is by design, though I can't find documentation in the manual. Equality assumptions (such as your k ~ Type) come into scope only in an expression of that type, not later on in the same type. This design significantly eased the implementation.

The second example should work -- that's a bug.

[RyanGlScott]

Forgive me if this is a silly question, but why shouldn't the first example work? I know that the implementation details would significantly complicate the story, but my perspective, being able to write the first example would make a lot of code easier to write. An example of this that came up in real code is when ​Edward Kmett tried to sketch out a solution to #13327 on the ghc-devs mailing list, and attempted to write this code:

class (Typeable t, Typeable k) => DataIfStar (k :: t) where
  dataIf :: (t ~ Type) => proxy k -> (Data k => r) -> r

But this won't work, because Data :: Type -> Constraint, and GHC isn't able to conclude that k :: t is actually k :: Type, since the evidence that t ~ Type isn't being used when typechecking.

If programs like these aren't supposed to typecheck by design, what is the workaround?

[RyanGlScott]

Another way to phrase my question is: I don't see what the distinction between the first and second examples is. After all, you can rewrite the second example like this:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

import Data.Kind (Type)
import Data.Typeable

foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
    => proxy a -> String
foo _ =
  case eqT :: Maybe (k :~: Type) of
    Nothing   -> "Non-Type kind"
    Just Refl -> go_on eqT
 where
  go_on :: k ~ Type => Maybe (a :~: Int) -> String
  go_on Nothing     = "Non-Int type"
  go_on (Just Refl) = "It's an Int!"

Now the equality assumption isn't coming into scope "only in an expression of that type", it's coming into scope in a type signature! So again, unless I'm misunderstanding something, I strongly suspect that fixing the second program would naturally lend itself towards fixing the first program.

[goldfire]

The problem is that a ~ b is a lifted type. That is, it contains bottom. So, when you write forall k (a :: k). k ~ Type => a -> a or some such, there's no place to check whether the proof of k ~ Type is valid before you use it. When an expression intervenes, then GHC can insert a case to evaluate the equality proof box to find the real primitive (~#) equality inside.

Some notes on this issue (intended solely as notes to self, so YMMV) are ​here.

So I don't agree that solving (2) will help with (1) here.

[RyanGlScott]

Ah, I completely overlooked bottoming equalities. Thanks for the reference.

In light of this, my "equivalent" program in comment:3 is not equivalent at all, since the k ~ Type evidence in go_on isn't known a priori to terminate, whereas in the original program, the equality is known not to bottom out by pattern matching on Refl.

So I suppose a better title for this bug would be "GHC doesn't think a type is of kind *, despite having Typeable-induced evidence for it", and the first program would be related to Dependent Haskell, which is, erm, in progress :)

[goldfire]

Theorem (Progress): For all research projects ρ, either ρ is published, or there exists a day δ such that ρ steps to ρ'.

Proof: Fix a given research project ρ. We now have two cases: either ρ is published, which trivially implies progress; or we must produce a day δ in which ρ will advance. We are done, choosing δ = tomorrow. QED.

So, yes, Dependent Haskell is in progress. And, yes, I agree with your other analysis in comment:5.

[simonpj]

Richard and I discussed the bug mentioned in comment:1. Solution

Don't do solveEqualities unless you are generalising (to solve #13337),
 in tc_hs_sig_type

Richard will work on this.

[goldfire]

Included in that work should be a check of all uses of solveEqualities to make sure that they make sense.

[Ben Gamari <ben@…>]

In e0c433c8/ghc:

Fix #13337.

The big change is the introduction of solveSomeEqualities. This
is just like solveEqualities, but it doesn't fail if there are unsolved
equalities when it's all done. Anything unsolved is re-emitted. This
is appropriate if we are not kind-generalizing, so this new form
is used when decideKindGeneralizationPlan says not to.

We initially thought that any use of solveEqualities would be tied
to kind generalization, but this isn't true. For example, we need
to solveEqualities a bunch in the "tc" pass in TcTyClsDecls (which
is really desugaring). These equalities are all surely going to be
soluble (if they weren't the "kc" pass would fail), but we still
need to solve them again. Perhaps if the "kc" pass produced type-
checked output that is then desugared, solveEqualities really would
be tied only to kind generalization.

Updates haddock submodule.

Test Plan: ./validate, typecheck/should_compile/T13337

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3315

[bgamari]

Merged to ghc-8.2 as 109a2429493c2a2d5481b67f5b0c1086a959813e.

[simonpj]

Modified by

commit 3cfee57abf00f794e7962e2a60efd9d7d8baf06f
Author: Richard Eisenberg <rae@cs.brynmawr.edu>
Date:   Thu Mar 16 15:56:37 2017 -0400

    Remove solveSomeEqualities
    
    I had thought that it was necessary to solve kind-level equalities
    before validity-checking a type, but I was wrong. This patch simply
    deletes code. Hooray!

Has this been merged?

[bgamari]

Indeed, that was merged to ghc-8.2 as 6c41ed6e7994451f78af87bff43d6baef19b8f0f.

[Simon Peyton Jones <simonpj@…>]

In 1e06d8b8/ghc:

Simplify the logic for tc_hs_sig_type

In fixing Trac #13337, and introducing solveSomeEqualities,
Richard introduce the higher-order function tc_hs_sig_type_x,
with a solver as its argument.

It turned out that there was a much simpler way to do the
same thing, which this patch implements.  Less code, easier
to grok.  No change in behaviour though.

[simonpj]

Not worth merging this to the 8.2 branch, I think. It's just refactoring.

[RyanGlScott]

See #12677 for a proper ticket devoted to the (k ~ Type) issue.