[GHC] #13952: Liberal coverage condition fails if TypeInType is enabled
#13952: Liberal coverage condition fails if TypeInType is enabled -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 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: -------------------------------------+------------------------------------- The following program compiles with 8.0.2 but fails with 8.2.1-rc2. It succeeds if the `TypeInType` extension is disabled. {{{#!hs {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, TypeFamilies, TypeOperators #-} -- Removing TypeInType causes compilation to succeed {-# LANGUAGE TypeInType #-} module Bookkeeper.Internal where import GHC.Generics import GHC.TypeLits (Symbol, KnownSymbol, TypeError, ErrorMessage(..)) class FromGeneric a book | a -> book where fromGeneric :: a x -> book type family Expected a where Expected (l :+: r) = TypeError ('Text "Cannot convert sum types into Books") Expected U1 = TypeError ('Text "Cannot convert non-record types into Books") instance (book ~ Expected U1) => FromGeneric U1 book where fromGeneric = error "impossible" }}} {{{ src/Bookkeeper/Internal.hs:18:10: error: • Illegal instance declaration for ‘FromGeneric U1 book’ The coverage condition fails in class ‘FromGeneric’ for functional dependency: ‘a -> book’ Reason: lhs type ‘U1’ does not determine rhs type ‘book’ Un-determined variable: book • In the instance declaration for ‘FromGeneric U1 book’ | 18 | instance (book ~ Expected U1) => FromGeneric U1 book where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} Perhaps this is related to #12803 but I made another ticket so that it can be diagnosed separately. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13952 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13952: Liberal coverage condition fails if TypeInType is enabled -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: fixed | 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => fixed Comment: This is expected behavior (see [https://github.com/GetShopTV/swagger2/issues/95 here] for another place where a similar issue arose). The difference between GHC 8.0 and 8.2 is that the datatypes in `GHC.Generics` are now poly-kinded. As a result, the kinds involved in `Expected` are generalized even further: the return kind of `Expected U1` does not determine the kind of `k` in `U1`'s kind (`k -> Type`), causing the liberal coverage condition to fail. This is more apparent if you turn on `-fprint-explicit-kinds`: {{{ $ /opt/ghc/8.2.1/bin/ghci Foo.hs -fprint-explicit-kinds GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bookkeeper.Internal ( Foo.hs, interpreted ) Foo.hs:19:10: error: • Illegal instance declaration for ‘FromGeneric k (U1 k) book’ The liberal coverage condition fails in class ‘FromGeneric’ for functional dependency: ‘a -> book’ Reason: lhs type ‘U1 k’ does not determine rhs type ‘book’ Un-determined variable: book • In the instance declaration for ‘FromGeneric U1 book’ | 19 | instance (book ~ Expected U1) => FromGeneric U1 book where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} This also explains why turning off `TypeInType` fixes the issue, since this kind generalization doesn't occur, and all of the kind variables simply default to `Type`. A simple way to fix this is to just be more explicit about what kinds to use in `Expected`: {{{#!hs type family Expected (a :: k -> Type) :: k where Expected ((l :+: r) :: k -> Type) = (TypeError ('Text "Cannot convert sum types into Books") :: k) Expected (U1 :: k -> Type) = (TypeError ('Text "Cannot convert non-record types into Books") :: k) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13952#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC