Opened 2 years ago

Last modified 5 months ago

#10227 new bug

Type checker cannot deduce type

Reported by: augustss Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.1
Keywords: InjectiveFamilies Cc: adamgundry, nfrisby
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (4)

comment:1 Changed 2 years ago by simonpj

True. Jan Stolarek's work on injective type families is a start in that direction.

But you want more. Would you care to write a specification of exactly what you want, and an algorithm for achieving it?

Simon

comment:2 Changed 2 years ago by adamgundry

Cc: adamgundry added

One can go arbitrarily far in this direction, so it's not obvious when to stop. I agree that D d Double ~ Bool seems like it should be easily solved, but what about something like D d Double ~ D d Bool? This also can hold only if d ~ In, which could be detected by unifying stuck closed type family applications with each branch in turn and noticing that all but one lead to inconsistencies.

I think this approach makes sense in terms of "improvement", but representing evidence for it would be difficult, so it would be hard to handle givens as opposed to wanteds. Moreover, it might not be very efficient!

If anyone would like to experiment, though, this seems like a nice application for typechecker plugins.

comment:3 Changed 2 years ago by nfrisby

Cc: nfrisby added

comment:4 Changed 5 months ago by simonpj

Keywords: InjectiveFamilies added
Note: See TracTickets for help on using tickets.