[GHC] #12055: Typechecker panic instead of proper error
#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
#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
#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: | -------------------------------------+------------------------------------- Comment (by simonpj): Well HEAD for this gives {{{ T12055.hs:18:1: error: • Non type-variable argument in the constraint: Category (Dom f) (Use FlexibleContexts to permit this) • In the context: (Category (Dom f), Category (Cod f)) While checking the super-classes of class ‘Functor’ In the class declaration for ‘Functor’ T12055.hs:26:1: error: • Fundeps in class ‘Fun’ (Use FunctionalDependencies to allow fundeps) • In the class declaration for ‘Fun’ T12055.hs:29:5: error: • Illegal instance declaration for ‘Fun p q f’ (All instance types must be of the form (T a1 ... an) where a1 ... an are *distinct type variables*, and each type variable appears at most once in the instance head. Use FlexibleInstances if you want to disable this.) • In the instance declaration for ‘Fun (p :: Cat j) (q :: Cat k) (f :: j -> k)’ }}} And if you add the missing language extensions {{{ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} }}} then it compiles cleanly. I suppose someone could bisect their way to the patch that fixed HEAD. Or we could just leave it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12055#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#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: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#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: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash | polykinds/T12055, T12055a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => polykinds/T12055, T12055a Comment: I've added two regressions test. HEAD is fine, but there really is a bug in GHC 8.0, producing "GHC internal error" when `FlexibleContexts` is omitted. It doesn't look that high a priority to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12055#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12055: Typechecker panic instead of proper error -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: lowest | Milestone: 8.0.3 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash | polykinds/T12055, T12055a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * priority: normal => lowest * milestone: 8.0.2 => 8.0.3 Comment: It looks like this won't happen for 8.0.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12055#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12055: Typechecker panic instead of proper error -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: merge Priority: lowest | Milestone: 8.0.3 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash | polykinds/T12055, T12055a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12055#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC