Opened 2 months ago

Last modified 2 months ago

#14451 new bug

Type synonym of type family causes error, error jumps to (fairly) unrelated source location

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


{-# 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:  :? 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.

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 (3)

comment:1 Changed 2 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:  :? 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 2 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 2 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.

Note: See TracTickets for help on using tickets.