Opened 13 months ago

Closed 13 days ago

#14451 closed bug (fixed)

Need proper SCC analysis of type declarations, taking account of CUSKs

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.2.1
Keywords: TypeInType, CUSKs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T14451
Blocked By: Blocking:
Related Tickets: #7503 Differential Rev(s):
Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

Description

{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}

import Data.Kind

data TyFun :: Type -> Type -> Type

type a ~> b = TyFun a b -> Type

type Cat ob = ob -> ob -> Type

type family 
  Apply (f :: a ~> b) (x :: a) :: b where
  Apply (CompSym2 f g) a = Comp f g a

data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c) 

type a·b = Apply a b 

class Varpi (f :: i ~> j) where
  type Dom (f :: i ~> j) :: Cat i
  type Cod (f :: i ~> j) :: Cat j

  varpa :: Dom f a a' -> Cod f (f·a) (f·a')

type family 
  Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where
  Comp f g a = f · (Apply g a)

This compiles, but if I replace the final line by

  Comp f g a = f · (g · a)

oddly enough I get an error message about the method varpa! Seemingly unrelated apart from using (·):

$ ghci2 hs/093-bug.hs
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/093-bug.hs, interpreted )

hs/093-bug.hs:23:33: error:
    • Expected kind ‘i ~> i’, but ‘f’ has kind ‘i ~> j’
    • In the first argument of ‘(·)’, namely ‘f’
      In the second argument of ‘Cod’, namely ‘(f · a)’
      In the type signature:
        varpa :: Dom f a a' -> Cod f (f · a) (f · a')
   |
23 |   varpa :: Dom f a a' -> Cod f (f·a) (f·a')
   |                                 ^
Failed, 0 modules loaded.
Prelude> 

NOW — let's randomly remove both lines that mention CompSym2 and it mysteriously works, again!

Apply and (·) seem to be equal up to variable names, I can't spot why

>> :set -fprint-explicit-foralls 
>> :set -fprint-explicit-kinds 
>> :set -fprint-explicit-coercions 
>> 
>> :kind Apply
Apply :: forall {a} {b}. (a ~> b) -> a -> b
>> :kind (·)
(·) :: forall {a} {k}. (a ~> k) -> a -> k

but it works if I define (·) as a type family rather than a synonym:

type family
  (f::a ~> b) · (x::a) :: b where
  f · x = Apply f x

so it's some difference between synonyms and TFs, but is it intentional? It's certainly odd how the error messages jumped the varpa method when we actually modified Comp.

Change History (9)

comment:1 Changed 13 months ago by RyanGlScott

The error message thing is a red herring: the real culprit is lurking in this slightly minimized version of your program:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind

data TyFun :: Type -> Type -> Type

type a ~> b = TyFun a b -> Type

type family
  Apply (f :: a ~> b) (x :: a) :: b where
  Apply (CompSym2 f g) a = Comp f g a

data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c)

type (a :: k1 ~> k2) · (b :: k1) = Apply a b

type family
  Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where
  Comp f g a = f · (g · a)

This appears to typecheck without issues. But there actually is an issue, if you poke around inside the file with GHCi:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :k (·)
(·) :: (k2 ~> k2) -> k2 -> k2

Egad! Despite the fact that we've appeared to give (·) the kind (k1 ~> k2) -> k1 -> k2, GHC somehow concludes that it actually has the more restrictive kind (k2 ~> k2) -> k2 -> k2. (This, in turn, causes the strange error message you've observed.)

As far as why this happens, my shot-in-the-dark guess is that this is a manifestation of #11203/#11453. But I'd need Richard to confirm this.

comment:2 Changed 13 months ago by goldfire

Keywords: TypeInType added

Yes, this could be #11203, but I haven't done enough analysis to be sure.

comment:3 Changed 13 months ago by simonpj

I don't think this is #11203. Here's what I think is happening

  • Apply, Comp, and OO (which I will use instead of the unicode dot symbol) are mutually

recursive, and so are kind-checked together.

  • The first two have CUSKs and so getInitialKinds gives them polykinds, thus
    kcTyClGroup: initial kinds
      [r1 :-> ATcTyCon Apply :: forall a b. (a ~> b) -> a -> b,
       r2 :-> ATcTyCon Comp :: forall k1 k2 k.
                               (k1 ~> k) -> (k2 ~> k1) -> k2 -> k,
       r4 :-> ATcTyCon OO :: k_aYg[tau:1] -> k_aYh[tau:1] -> k_aYi[tau:1]]
    
    Good so far.
  • But then pathetically, we run over all three declarations, gathering constraints on the kind variables in OO. In the end we make OO insufficiently polymorphic, giving it kind
      OO :: forall b. (b ~> b) -> b -> b
    
    whereas it should have kind
      OO :: forall a b. (a ~> b) -> a -> b
    
    That's stupid: OO's kind should obviously be the same as Apply's

What we should do is exactly what we do for value declarations:

  • Take the SCC (the group of three declarations)
  • Remove edges that point to type constructors that have a CUSK
  • Do a new SCC on this thinned-out graph.
  • Now OO will be first, in a SCC by itself, because Apply and Comp depend on it, but not vice versa (after removing those edges)
  • Now kind-check each smaller SCC one by one, generalising each in turn.

For bindings you can see the extra SCC analysis being done in TcBinds.tc_group.

So all we have to do is to replicate this logic for types. Fiddly, perhaps, but not difficult.

comment:4 Changed 10 months ago by simonpj

Summary: Type synonym of type family causes error, error jumps to (fairly) unrelated source locationNeed proper SCC analysis of type declarations, taking account of CUSKs

See also #7503

comment:5 Changed 10 months ago by kcsongor

Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

comment:6 Changed 7 months ago by RyanGlScott

Keywords: CUSKs added

comment:7 Changed 2 weeks ago by RyanGlScott

Amazingly, the original program in this ticket (including the Comp f g a = f · (g · a) tweak):

{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs, RankNTypes, UndecidableInstances #-}

import Data.Kind

data TyFun :: Type -> Type -> Type

type a ~> b = TyFun a b -> Type

type Cat ob = ob -> ob -> Type

type family
  Apply (f :: a ~> b) (x :: a) :: b where
  Apply (CompSym2 f g) a = Comp f g a

data CompSym2 :: (b ~> c) -> (a ~> b) -> (a ~> c)

type a·b = Apply a b

class Varpi (f :: i ~> j) where
  type Dom (f :: i ~> j) :: Cat i
  type Cod (f :: i ~> j) :: Cat j

  varpa :: Dom f a a' -> Cod f (f·a) (f·a')

type family
  Comp (f::k1 ~> k) (g::k2 ~> k1) (a::k2) :: k where
  Comp f g a = f · (g · a)

Appears to have fixed itself at some point between GHC 8.4 and 8.6, since it typechecks on GHC 8.6.2 and HEAD. I'm not sure what commit caused that, but that's cool nonetheless.

Let me check to see if the same miracle happened to #7503.

comment:8 Changed 13 days ago by Ryan Scott <ryan.gl.scott@…>

In aef5d825/ghc:

Add test cases for #7503, #14451

At some point between 8.4 and 8.6, two things were fixed:

* The entirety of #14451.
* One of the test cases in #7503. I've added this as T7503a. The
  other test case from that ticket still does /not/ work, so we'll
  have to add T7503b some other day.

comment:9 Changed 13 days ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T14451

Alas, #7503 was not entirely fixed—see https://ghc.haskell.org/trac/ghc/ticket/7503#comment:10. But this ticket is entirely fixed, so we can close this one now.

Note: See TracTickets for help on using tickets.