[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 (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------
Description changed by bgamari:

@@ -65,0 +65,15 @@
+
+ If one adds the appropriate extensions (`FunctionalDependencies`,
+ `FlexibleInstances`, and `FlexibleContexts`) GHC complains that the
+ program fails to satisfy the coverage condition,
+ {{{
+ Hi.hs:31:10: error:
+     • Illegal instance declaration for ‘Fun k j p q f’
+         The coverage condition fails in class ‘Fun’
+           for functional dependency: ‘f -> p q’
+         Reason: lhs type ‘f’ does not determine rhs types ‘p’, ‘q’
+         Un-determined variables: p, q
+         Using UndecidableInstances might help
+     • In the instance declaration for
+         ‘Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)’
+ }}}

New description:

 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’
 }}}

 If one adds the appropriate extensions (`FunctionalDependencies`,
 `FlexibleInstances`, and `FlexibleContexts`) GHC complains that the
 program fails to satisfy the coverage condition,
 {{{
 Hi.hs:31:10: error:
     • Illegal instance declaration for ‘Fun k j p q f’
         The coverage condition fails in class ‘Fun’
           for functional dependency: ‘f -> p q’
         Reason: lhs type ‘f’ does not determine rhs types ‘p’, ‘q’
         Un-determined variables: p, q
         Using UndecidableInstances might help
     • In the instance declaration for
         ‘Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)’
 }}}

--

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