Type checker cannot deduce type

When using closed type families the type checker does not use all the information that the closedness condition implies.

In the following module the type checker fails to deduce the type for f.

But lets start with descrIn since it has the same problem. The deduced type is (D d Bool ~ Bool, D d Double ~ Bool, D d (Maybe String) ~ Bool) => Descr d. But it is (to quote Simon PJ) plain as a pikestaff that D d Double ~ Bool can only hold if d ~ In, since there are only two equations and it cannot be the second.

Similar reasoning can be used to deduce all the commented out type signatures.

{-# LANGUAGE RecordWildCards, TypeFamilies, DataKinds, NoMonomorphismRestriction, FlexibleContexts #-}
module Main(main) where
import Data.Maybe

data InOut = In | Out

type family D (d :: InOut) a where
    D 'In  a = Bool
    D 'Out a = a

data Descr d = Descr {
    abc :: D d Bool,
    def :: D d Double,
    ghi :: D d (Maybe String)
    }

--descrIn :: Descr 'In
descrIn = Descr { abc = False, def = True, ghi = True }

--f :: Descr 'Out -> Double
f Descr{..} = def + read (fromMaybe "0" ghi)

--g :: Descr 'In -> Descr 'Out
g d = Descr { abc = if abc d then True else False,
              def = if def d then 1234 else 0,
              ghi = if ghi d then Just "3008" else Nothing }

main :: IO ()
main = do
    print $ f $ g descrIn

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture