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

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

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture