Opened 5 months ago

Closed 5 months ago

#13879 closed bug (fixed)

Strange interaction between higher-rank kinds and type synonyms

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

Description

Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:

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

import Data.Kind

data family Sing (a :: k)

data (a :: j) :~~: (b :: k) where
  HRefl :: a :~~: a

data instance Sing (z :: a :~~: b) where
  SHRefl :: Sing HRefl

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> p HRefl
          -> p r
(%:~~:->) SHRefl pHRefl = pHRefl

type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x

Now I want to refactor this so that I use App:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> App p HRefl
          -> App p r

However, GHC doesn't like that:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:21:20: error:
    • Expected kind ‘(:~~:) j z a a’,
        but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’
    • In the second argument of ‘App’, namely ‘HRefl’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> App p HRefl -> App p r
   |
21 |           -> App p HRefl
   |                    ^^^^^

Bug.hs:22:20: error:
    • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’
    • In the second argument of ‘App’, namely ‘r’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> App p HRefl -> App p r
   |
22 |           -> App p r
   |                    ^

These errors are surprising to me, since it appears that the two higher-rank types, z and y, are behaving differently here: y appears to be willing to unify with other types in applications of p, but z isn't! I would expect both to be willing to unify in applications of p.

Out of desperation, I tried this other formulation of (%:~~:->) which uses HRApp instead of App:

(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
             Sing r
          -> HRApp p HRefl
          -> HRApp p r

But now I get an even stranger error message:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:21:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
21 |           -> HRApp p HRefl
   |                    ^

Bug.hs:21:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
21 |           -> HRApp p HRefl
   |                    ^

Bug.hs:22:20: error:
    • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
        but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
    • In the first argument of ‘HRApp’, namely ‘p’
      In the type signature:
        (%:~~:->) :: forall (j :: Type)
                            (k :: Type)
                            (a :: j)
                            (b :: k)
                            (r :: a :~~: b)
                            (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
                     Sing r -> HRApp p HRefl -> HRApp p r
   |
22 |           -> HRApp p r
   |                    ^

That's right, it can't match the kinds:

  • forall z (y :: z). (:~~:) j z a y -> *, and
  • forall z (y :: z). (:~~:) j z a y -> *

Uh... what? Those are the same kind!

Change History (7)

comment:1 Changed 5 months ago by simonpj

I could not resist investigating. Here are my conclusions.

  • With a DEBUG compiler, I immediately tripped over
    	ASSERT failed!
      in_scope InScope {z_aUa y_aUb}
      tenv [aSo :-> z0_aUa[tau:1], aSp :-> y0_aUb[tau:1]]
      cenv []
      tys [(:~~:) j0_aU1[tau:1] k0_aU2[tau:1] a_aSl[sk:1] y_aSp[sk:1]
           -> *]
      cos []
      needInScope [aSj :-> j_aSj[sk:1], aSl :-> a_aSl[sk:1],
                   aU1 :-> j_aU1[tau:1], aU2 :-> k_aU2[tau:1]]
      Call stack:
          CallStack (from HasCallStack):
            prettyCurrentCallStack, called at compiler\utils\Outputable.hs:1133:58 in ghc:Outputable
            callStackDoc, called at compiler\utils\Outputable.hs:1188:22 in ghc:Outputable
            assertPprPanic, called at compiler\types\TyCoRep.hs:2099:51 in ghc:TyCoRep
            checkValidSubst, called at compiler\types\TyCoRep.hs:2122:29 in ghc:TyCoRep
            substTy, called at compiler\typecheck\TcHsType.hs:936:27 in ghc:TcHsType
    
    This was just a missing in-scope set setup in TcHsType.instantiateTyN. Easy to fix.
  • Next up, the original program. The bug here was that in a type signature like
         f :: forall (p :: forall z (y::z). <blah>). <more blah>
    
    when instanting p's kind at occurrences of p in <more blah> it's crucial that the kind we instantiate is fully zonked, else we may fail to substitute properly. But tcLHsKind (which converts the LHsKind to a Kind didn't zonk its result. Also easily fixed, and that makes the original program work.
  • Next, the mysterious message when you use HRApp. This arises because we try to unify the kinds
        forall z1 (y1::z1). HR a1 b1 c1 d1  ~#  forall z2 (y2::z2). HR a2 b2 c2 d2
    
    (I'm using HR instead of infix :~~:, just to keep my head straight.) The first thing is that, at least by the time the constraint solver gets it, if we zonked LHS and RHS we'd see they were equal. But that's a small thing. What we do in TcCanonical is this:
    can_eq_nc' _flat _rdr_env _envs ev eq_rel
                 s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
     | CtWanted { ctev_loc = loc, ctev_dest = orig_dest } <- ev
     = do { let (bndrs1,body1) = tcSplitForAllTyVarBndrs s1
                (bndrs2,body2) = tcSplitForAllTyVarBndrs s2
          ; kind_cos <- zipWithM (unifyWanted loc Nominal)
                                 (map binderKind bndrs1) (map binderKind bndrs2)
          ; all_co <- deferTcSForAllEq (eqRelRole eq_rel) loc
                                        kind_cos (bndrs1,body1) (bndrs2,body2)
          ; setWantedEq orig_dest all_co
          ; stopWith ev "Deferred polytype equality" }
    
    Look at that zipWithM. It's obvously bogus in the case above, because we produce a constraint z1~z2 which is insoluble.

I need Richard's help here; but I think we just need to spit out that kind equality inside the new implication constraint, and after the alpha-renaming, rather than outside and before.

comment:2 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In 4bdac331/ghc:

Fix the in-scope set in TcHsType.instantiateTyN

See Trac #13879

comment:3 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In c80920d2/ghc:

Do zonking in tcLHsKindSig

Trac #13879 showed that there was a missing zonk in tcLHsKind.

I also renamed it to tcLHsKindSig, for consistency with type signatures
There's a commment to explain why the zonk is needed.

comment:4 Changed 5 months ago by Simon Peyton Jones <simonpj@…>

In fae672f/ghc:

Fix constraint solving for forall-types

Trac #13879 showed that when we were trying to solve

  (forall z1 (y1::z1). ty1)  ~  (forall z2 (y2:z2). ty2)

we'd end up spitting out z1~z2 with no binding site for them.
Those kind equalities need to be inside the implication.

I ended up re-factoring the code for solving forall-equalities.
It's quite nice now.

comment:5 Changed 5 months ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T13879

All done!

Probably worth merging these patches; I'm pretty sure they won't trigger new bugs.

comment:6 Changed 5 months ago by RyanGlScott

Milestone: 8.2.1
Note: See TracTickets for help on using tickets.