Re: [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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

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

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

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