Opened 7 months ago

Closed 6 months ago

Last modified 3 months ago

#13337 closed bug (fixed)

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

Reported by: RyanGlScott Owned by: goldfire
Priority: normal Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.0.2
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #12677 Differential Rev(s): Phab:D3315
Wiki Page:

Description

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!

Change History (18)

comment:1 Changed 7 months ago by 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.

comment:2 Changed 7 months ago by 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?

comment:3 Changed 7 months ago by 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.

Last edited 7 months ago by RyanGlScott (previous) (diff)

comment:4 Changed 7 months ago by 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.

comment:5 Changed 7 months ago by 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 :)

comment:6 Changed 7 months ago by 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.

comment:7 Changed 7 months ago by 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.

comment:8 Changed 7 months ago by goldfire

Owner: set to goldfire

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

comment:9 Changed 7 months ago by simonpj

Keywords: TypeInType added

comment:10 Changed 7 months ago by goldfire

Differential Rev(s): Phab:D3315
Status: newpatch

comment:11 Changed 6 months ago by bgamari

Milestone: 8.2.1

comment:12 Changed 6 months ago by 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

comment:13 Changed 6 months ago by bgamari

Resolution: fixed
Status: patchclosed

comment:14 Changed 6 months ago by simonpj

Status: closedmerge

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?

comment:15 Changed 6 months ago by bgamari

Status: mergeclosed

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

comment:16 Changed 6 months ago by 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.

comment:17 Changed 6 months ago by simonpj

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

comment:18 Changed 3 months ago by RyanGlScott

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

Note: See TracTickets for help on using tickets.