#15905: Data familes should end in Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14645 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Some thoughts from this morning's call: * The error report in the original report is unrelated to this ticket: it's just #12088 again. Adding a TH splice does the trick, giving this minimal example: {{{#!hs {-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TemplateHaskell #-} module Bug where import Data.Kind data family Fix (f :: Type -> k) :: k type family F a type instance F Int = Type -> Type $(return []) data instance Fix (f :: Type -> F Int) (x :: Type) = Mk }}} This is accepted, by transforming the instance to {{{#!hs data instance Fix @(Type -> Type) (f :: Type -> Type) (x :: Type) = Mk }}} In other words, GHC just realizes it can replace `F Int` with `Type -> Type` and carry on. * In an attempt to stop GHC from being this clever, we tried using visible dependent quantification: {{{#!hs data family Fix k (f :: Type -> k) :: k data instance Fix (F Int) (f :: Type -> F Int) (x :: Type) = Mk }}} Note that `k` is explicit now. This panics, because the `unravelFamInstPats` chokes on the strange instance, causing downstream chaos. (Really, `unravelFamInstPats` should panic.) However, if somehow the plumbing were fixed, this would be rejected because it mentions a type family in a type pattern. * In another attempt to defeat the ever-clever GHC, I tried using an explicit forall. {{{#!hs data family Fix (f :: Type -> k) :: k data instance forall (f :: Type -> F Int) (x :: Type). Fix f x = Mk }}} This works by instantiating `Fix` with `Type -> Type` (as before) and casting `f`. * Previously, Simon was worried about the fact that there might be a difference in behavior between eager unification and the work the solver does. But I don't think there is, as `solveEqualities` is called ''before'' `unravelFamInstPats`. * The problem here is really all about when type families get in the way of exposing arrows in the data family's kind. In the `Fix` example, the type family `F Int` obscures the underlying type `Type -> Type`. How do we specify when such a problem exists? * I conjecture that the problem never exists on its own. This obfuscation can happen only in two ways: (1) either some kind parameter has been instantiated with a type family application, or (2) a type family application appears in the return kind of a data family. In case (1), we're blocked by #12564; that case cannot happen. In case (2), we're blocked by #14645. So I think that this ticket, by itself, is redundant currently. If either of those other tickets is fixed, it won't be. * Fixing #12564 is likely to require generalizing (or otherwise changing) the form of type family LHSs, thus fixing this ticket inter alia. So, the upshot is: let's fix #12564 before #14645, and this ticket never needs to be considered again. :) I'm commenting on those two tickets, too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15905#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler