[GHC] #12055: Typechecker panic instead of proper error

[GHC]

#12055: Typechecker panic instead of proper error
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.0.2
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider this modification of the testcase from #12021,
 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeInType #-}

 import GHC.Base ( Constraint, Type )
 import GHC.Exts ( type (~~) )

 type Cat k = k -> k -> Type

 class Category (p :: Cat k) where
     type Ob p :: k -> Constraint

 class (Category (Dom f), Category (Cod f)) => Functor (f :: j -> k) where
     type Dom f :: Cat j
     type Cod f :: Cat k
     functor :: forall a b.
                Iso Constraint (:-) (:-)
                (Ob (Dom f) a)     (Ob (Dom f) b)
                (Ob (Cod f) (f a)) (Ob (Cod f) (f b))

 class (Functor f , Dom f ~ p, Cod f ~ q) =>
     Fun (p :: Cat j) (q :: Cat k) (f :: j -> k) | f -> p q
 instance (Functor f , Dom f ~ p, Cod f ~ q) =>
     Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)

 data Nat (p :: Cat j) (q :: Cat k) (f :: j -> k) (g :: j -> k)

 type Iso k (c :: Cat k) (d :: Cat k) s t a b =
     forall p. (Cod p ~~ Nat d (->)) => p a b -> p s t

 data (p :: Constraint) :- (q :: Constraint)
 }}}
 With GHC 8.0.1 it fails with a compiler panic,
 {{{
 $ ghc Hi.hs -fprint-explicit-kinds
 [1 of 1] Compiling Main             ( Hi.hs, Hi.o )

 Hi.hs:21:1: error:
     • Non type-variable argument
         in the constraint: Category j (Dom k j f)
       (Use FlexibleContexts to permit this)
     • In the context: (Category j (Dom k j f), Category k (Cod k j f))
       While checking the super-classes of class ‘Functor’
       In the class declaration for ‘Functor’

 Hi.hs:29:20: error:
     • GHC internal error: ‘Dom’ is not in scope during type checking, but
 it passed the renamer
       tcl_env of environment: [a2yi :-> Type variable ‘j’ = j,
                                a2yj :-> Type variable ‘p’ = p, a2yk :->
 Type variable ‘k’ = k,
                                a2yl :-> Type variable ‘q’ = q, a2ym :->
 Type variable ‘f’ = f,
                                r2xT :-> ATcTyCon Fun]
     • In the first argument of ‘~’, namely ‘Dom f’
       In the class declaration for ‘Fun’
 }}}

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