Type family not reduced, again

This one looks similar to #12381 (closed), but unfortunately, it does not seem to be fixed in HEAD:

{-# LANGUAGE TypeInType, TypeFamilies, FlexibleInstances #-}

import GHC.Types

type family F (a :: Type) :: Type

class C a where
  type D (a :: Type) :: F a

instance (F a ~ Bool) => C a where
  type D a = True

This yields (in 8.0.1 and 8.1.20160709):

Constraint.hs:11:14: error:
    • Expected kind ‘F a’, but ‘'True’ has kind ‘Bool’
    • In the type ‘True’
      In the type instance declaration for ‘D’
      In the instance declaration for ‘C a’

changed weight to 5

added Tbug Trac import labels

mentioned in issue #12385 (closed)

changed the description

#12381 (closed) and #11348 (closed) were all about the order in which instance declarations are checked, but this case seems to be something different. Here there's no choice but to check these declarations in the order that they're written: the type family, then the class, then the instance of that class.

I suppose the type of D () should be (F a ~ Bool) => True but as far as I know GHC can't handle such a thing.

mentioned in issue #12432 (closed)

closed

Yes, I think this is something we simply don't support at all.

Associated type declarations are just a way to remind you to add type instance decl for D whenever you make an instance decl for C. It's always equivalent to doing it separately, thus:

type instance D a = True
instance (F a ~ Bool) => C a where

And you can see that this isn't going to work.

The point is that (F a ~ Bool) is has local evidence, bound by the dictionary lambda for the instance dfun. That evidence can't be used in a type instance decl.

So I'll close this as invalid, but you can re-open as a feature request if (a) you think it's important, (b) you can specify what it does, and (c) you can extend System FC to support it.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label