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 |