[GHC] #10227: Type checker cannot deduce type

2 Apr 2015

      #10227: Type checker cannot deduce type
-------------------------------------+-------------------------------------
              Reporter:  augustss    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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.

 {{{#!hs
 {-# 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
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10227
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler