Opened 7 months ago

Closed 5 months ago

#13333 closed bug (fixed)

Typeable regression in GHC HEAD

Reported by: RyanGlScott Owned by: goldfire
Priority: highest Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.1
Keywords: typeable, TypeInType Cc: bgamari, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T13333
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3424
Wiki Page:

Description (last modified by RyanGlScott)

I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded Typeable. This compiles without issue on GHC 8.0.1 and 8.0.2:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module DataCast where

import Data.Data
import GHC.Exts (Constraint)

data T (phantom :: k) = T

data D (p :: k -> Constraint) (x :: j) where
  D :: forall (p :: k -> Constraint) (x :: k). p x => D p x

class Possibly p x where
  possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)

dataCast1T :: forall k c t (phantom :: k).
              (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
           => (forall d. Data d => c (t d))
           -> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
                 Nothing -> Nothing
                 Just D  -> gcast1 f

But on GHC HEAD, it barfs this error:

$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast         ( Bug.hs, interpreted )

Bug.hs:28:29: error:
    • Could not deduce (Typeable T) arising from a use of ‘gcast1’
        GHC can't yet do polykinded Typeable (T :: * -> *)
      from the context: (Typeable k, Typeable t, Typeable phantom,
                         Possibly Data phantom)
        bound by the type signature for:
                   dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
                                  Possibly Data phantom) =>
                                 (forall d. Data d => c (t d)) -> Maybe (c (T phantom))
        at Bug.hs:(22,1)-(25,35)
      or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
        bound by a pattern with constructor:
                   D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x,
                 in a case alternative
        at Bug.hs:28:23
    • In the expression: gcast1 f
      In a case alternative: Just D -> gcast1 f
      In the expression:
        case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
          Nothing -> Nothing
          Just D -> gcast1 f
   |
28 |                  Just D  -> gcast1 f
   |                             ^^^^^^^^

That error message itself is hilariously strange, since GHC certainly has the power to do polykinded Typeable nowadays.

Marking as high priority since this is a regression—feel free to lower the priority if you disagree.

Change History (18)

comment:1 Changed 7 months ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 7 months ago by RyanGlScott

I've observed something even stranger about this program. Let's tweak it slightly and add a couple more things (note that the definition of dataCast1T is unchanged):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module DataCast where

import Data.Data
import GHC.Exts (Constraint)

data T (phantom :: k) = T

data D (p :: k -> Constraint) (x :: j) where
  D :: forall (p :: k -> Constraint) (x :: k). p x => D p x

class Possibly p x where
  possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)

instance Possibly Data () where
  possibly _ _ = Just D

dataCast1T :: forall k c t (phantom :: k).
              (Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
           => (forall d. Data d => c (t d))
           -> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
                 Nothing -> Nothing
                 Just D  -> gcast1 f

newtype Q q x = Q { unQ :: x -> q }
ext1Q :: (Typeable k, Typeable t, Typeable (phantom :: k), Possibly Data phantom)
      => (T phantom -> q)
      -> (forall e. Data e => t e -> q)
      -> T phantom -> q
ext1Q def ext arg =
  case dataCast1T (Q ext) of
    Just (Q ext') -> ext' arg
    Nothing       -> def arg

With GHC HEAD, this gives the same error as the original program. But if you add this one definition to this file:

test1 :: Char
test1 = (const 'p') `ext1Q` (\T -> 'q') $ (T :: T ())

Then it typechecks without issue on GHC HEAD! This is pretty bizarre, considering that the error was originally reported in dataCast1T, and we managed to make the error go away without making a single change to dataCast1T.

FWIW, this program also compiles without issue on GHC 8.0.2 (with and without test1).

comment:3 Changed 7 months ago by bgamari

Keywords: typeable added

comment:4 Changed 6 months ago by bgamari

Owner: set to bgamari

comment:5 Changed 6 months ago by bgamari

Looking at -ddump-tc-trace from the program in the ticket description, it seems that we are failing to solve for this,

WC {wc_simple = 
      [WD] $dTypeable_a29a 
        {0}:: Typeable (T |> Trans (Sym cobox ->_N <*>_N)
                                   (cobox ->_N <*>_N)) (CDictCan)}

I believe the reason for this is that we don't handle casts in the Typeable solver. I'll need to think about this.

comment:6 Changed 6 months ago by simonpj

I think that if we have t :: k1 and c :: k1 ~ k2 and

Constraints:  [W] c :: Typeable k2 (t |> c)

then we can simplify the wanted constraint to

Bindings:    c = c1 |> Typeable ?? c
Constraints: [W] c1 :: Typeable k1 t

Richard do you agree? What is the ???

comment:7 Changed 6 months ago by simonpj

Also what if we have

Eq (t |> c)

Can we solve that, or do we get stuck?

comment:8 Changed 6 months ago by goldfire

I have a solution in progress. But no time to finish now. Soon. It involves adding a case for casts in matchTypeable. Not hard.

comment:9 Changed 5 months ago by goldfire

Differential Rev(s): Phab:D3424

I now think I know what's going on here, but unsure the best way to fix it. Interestingly, the problem has nothing to do with Typeable or TypeInType. Indeed it's amazing we've never hit this problem before.

We have

  [G] c1 :: k1[tau] ~ j1[tau]

in an implication. Both k1 and j1 are filled in at this point: k1 := Type and j1 := k2[sk]. This constraint is then passed through solveSimpleGivens, where it is canonicalized. can_eq_nc' flattens both sides, following both k1 and j1 to find Type. can_eq_nc' then calls rewriteEqEvidence which creates a new

  [G] c2 :: Type ~ k2[sk]

Of course, GHC produces evidence for c2: c2 = g1 ; c1 ; g2, where g1 and g2 are the coercions that come from flattening k1 and j1.

The problem is that these coercions, g1 and g2 are both reflexive, as they arise simply from zonking. See the line of code here. When c2 is stitched together from g1, c1, and g2, the calls to mkTcTransCo notice that some of the arguments are Refl, and so ignores the reflexive arguments. The end result is that c2 = c1. And then, when c2 gets put in the inert set, its kind still mentions unzonked variables. (Even though the associated ctPred is just fine.)

What to do? Here are some ideas:

  1. Stop mkTcTransCo (but not mkTransCo) from optimizing this case.
  1. Add a zonk somewhere (addInertEq? seems better than rewriteEqEvidence) to fix this problem.
  1. Add a new coercion form ZonkCo that relates an unzonked tyvar to its contents. This way, we can have the invariant that, whenever (ty', co) <- flatten ty, we have co :: ty' ~ ty. (Right now, that final equality is true only modulo zonking. But the new ZonkCo would allow it to be true without needing to zonk.) In fully-typechecked Core, ZonkCo would zonk to become reflexive, and so Core would have no ZonkCos.
  1. Add a new castTcCoercion function that stitches three coercions together using transitivity; this castTcCoercion would cleverly not optimize the Refl away.

I favor (1) but am worried about performance implications. (3) is probably the most principled, but it seems like a sledgehammer to tap in a nail. (4) is a middle ground, but I'm worried that what's happening here (a coercion returned from the flattener having an unzonked kind) happens elsewhere where we wouldn't use castTcCoercion.

What are your thoughts?

(NB: The patch linked to here does not have any of these fixes. I posted that patch some time ago but never added the link from this ticket.)

comment:10 Changed 5 months ago by simonpj

The end result is that c2 = c1. And then, when c2 gets put in the inert set, its kind still mentions unzonked variables. (Even though the associated ctPred is just fine.)

I don't see the problem. See Note [Ct/evidence invariant] in TcRnTypes. The types in evidence terms are no zonked, and that should not matter one whit.

Can you explain more precisely what actually goes wrong and why?

Simon

comment:11 Changed 5 months ago by goldfire

It turns out that Note is no longer true. See Phab:D3424 for more explanation. There are validation failures there I have not investigated yet.

comment:12 Changed 5 months ago by simonpj

I'm sorry, but I still don't get it. Why don't we fix the bug that makes the Note untrue? I do not understand why it's bad for an evidence term (which the constraint solver never looks at) to be Refl, if it relates two types that are equal after zonking.

Your diagnosis concludes

And then, when c2 gets put in the inert set, its kind still mentions unzonked variables.

But you do not say why that matters. I think it should not matter.

Can you explain more precisely what goes wrong and why?

comment:13 Changed 5 months ago by bgamari

Owner: changed from bgamari to goldfire
Priority: highhighest

Bumping the priority of this; I don't think we'll want to cut an 8.2-rc2 until this is fixed.

comment:14 Changed 5 months ago by simonpj

Keywords: TypeInType added

comment:15 Changed 5 months ago by bgamari

Status: newpatch

comment:16 Changed 5 months ago by Ben Gamari <ben@…>

In 09bf135a/ghc:

Fix #13333 by fixing the covar's type in ctEvCoercion

The change is noted in Note [Given in ctEvCoercion]. This patch
also adds a bit more commentary to TcFlatten, documenting some
key invariants of the flattening algorithm. While in the area,
I also removed some stale commentary from TcCanonical.

comment:17 Changed 5 months ago by goldfire

Status: patchmerge
Test Case: typecheck/should_compile/T13333

Thanks for pushing this, Ben!

comment:18 Changed 5 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.