[GHC] #14451: Type synonym of type family causes error, error jumps to (fairly) unrelated source location

11 Nov 2017

      #14451: Type synonym of type family causes error, error jumps to (fairly) unrelated
source location
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# 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

 {{{#!hs
   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:

 {{{#!hs
 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`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14451
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler