#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | PatternMatchWarnings 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 andrewthad): I guess `Any` isn't really a nullary type family since the `k` argument is invisible. So, the special case that needs to be handled to make this work is "all empty type families, regardless of arity". But I think it could be done a little more broadly. Playing with the type checker, I found that this compiles: {{{#!haskell {-# language DataKinds #-} {-# language TypeFamilies #-} module TypeEqualities where type family Foo (b :: Bool) :: Bool foo :: (Foo 'True ~ 'True, Foo 'True ~ Foo 'False) => Int foo = 5 }}} My interpretation of this is that type family applications that do not reduce are not considered apart from anything. The behavior that would help me is for non-reducing type family applications with constant arguments to be considered apart from everything except for themselves. Using the above example, `Foo 'True ~ Foo 'True` would typecheck, but `Foo 'True ~ 'True` and `Foo 'True ~ Foo 'False` would both be rejected. In bulleted form, the requirement I listed are: * Non-reducing (or stuck) * Constant arguments (yes: `Foo 'True`, no: `Foo x`) I'm not sure if this is introduces inconsistencies or has any negative side effects. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler