Haskell type family applications are not evaluated

Question

I found an interesting situation, when using data kinds with type families.

The compiler's error message is No instance for (C (ID ())) arising from a use of W. It suggests that a type family application is not fully evaluated, even when it is saturated. :kind! ID () evaluates to (), so according to the C () instance should be used.

{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances, FlexibleContexts #-}

type family ID t where
  ID t = t

class C t where
instance C () where

data W where
  W :: C (AppID t) => P t -> W

type family AppID t where
  AppID t = (ConstID t) ()

type family ConstID t where
  ConstID t = ID

data P t where
  P :: P t

data A

w :: W
w = W (P :: P A)

Could I somehow force the evaluation of ID ()? Is it a compiler bug?

I'm using GHC 7.8.3

Praedial

How does (ID ()) evaluate to anything? There are no instances for the ID family. – Atop

I wrote it as a closed type family (haskell.org/haskellwiki/GHC/…) – Raybin

Writing it as a normal type family does not change the error. – Raybin

Sorry, I didn't read your code carefully enough. Yeah, it looks like it should work. – Atop

Eta-expanding ConstID t seems to work. Maybe there is some bug in the handling of partially applied type families as in ID. (Honestly, I thought these were disallowed. Did we effectively get type-level lambdas lately?) – Thirtytwomo

As I see, most of what can be done on term level can also be done on type level. It's nice, isn't it? – Raybin

I say it's a bug. Also, try y = case W (P :: P A) of W P -> "hi" and weep at the resulting absurd error. – Audwin

Something more: if I leave the type signature w :: W it compiles. When I ask the type of w, it gives w :: W. – Raybin

Answer 1

The problem is the kind of ConstID.

type family ConstID t a where
  ConstID t a = ID a

Shermanshermie