#9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family -------------------------------------+------------------------------------- Reporter: qnikst | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by oleg): I too have tried to induce unsoundness with overlapping instances and concluded it is unlikely -- although there is plenty of strange and incoherent behavior one can observe. The straightforward attempt to pack an existential in one type class environment and unpack it in another module (where a more specialized instance is introduced) does not work because the existential is packed with the corresponding dictionary. When it is unpacked, the packed dictionary is used -- regardless how many new instances become available. Without type families, a type variable always stood for some ground type, at least potentially. When we assert a constraint C a on the type variable a, that constraint will not be dropped or discarded. It will be explicitly passed around, until it is resolved (or cannot be resolved -- in which case an error is reported). That is why it is safe to do instance selection for unground types: if we have {{{ class C a where foo :: a -> Int instance C [a] where foo = length test3 x = foo [x] }}} the inferred type for test3 :: t -> Int has no constraints. We resolved C [t] for the unground type t. If t had other constraints, they will be preserved. With type functions, we are no longer sure what the type variable represents. It can be a non-reduced type-function application. So a type variable now stands not for a value (ground type) but for an expression. And that could be a problem. For example: {{{ type family TT a -- no instances newtype D a = D{unD:: [TT a]} test4 (x::a) = foo (unD (undefined:: D a)) test5 (x::a) = foo (unD (D []:: D a)) }}} The code type-checks and test5 () even runs, returning 0. So, although T a has no instances, we have successfully ignored that fact. That trick would not have worked with only type classes; if we add a constraint we can't cast it away, and the type checker will demand sooner or later the constraint be satisfied. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler