#7288: type inference fails with where clause (RankNTypes, TypeFamilies)
----------------------------------------+-----------------------------------
Reporter: agrafix | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.6.1
Resolution: invalid | Keywords: type inference,
rankntypes, typefamilies
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Changes (by simonpj):
* status: new => closed
* difficulty: => Unknown
* resolution: => invalid
Old description:
> when using RankNTypes and TypeFamilies with polymorphic functions, type
> inference works in let but not in where clauses.
>
> {{{
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE TypeFamilies #-}
>
> import Control.Monad
>
> class Monad m => GenM m where
> type GenReq m :: *
>
> type GenFun a b = forall m. GenM m => a -> m b
> data GenDef a b = GenDef { name :: String, fun :: GenFun a b }
> data Gen a b = Gen
> data Struct = Struct
>
> mkGen :: forall a b. String -> GenFun a b -> GenDef a b
> mkGen = GenDef
>
> runGen :: GenM m => Gen a b -> a -> m (Maybe b)
> runGen = undefined
>
> getPatients :: GenM m => m [Int]
> getPatients = undefined
>
> -- BROKEN
> myGen :: Gen String Struct -> GenDef Int [Struct]
> myGen structGen =
> mkGen "myGen" $ \pid ->
> do pats <- getPatients
> structs <- mapM patToStruct pats
> return structs
> where
> patToStruct pid =
> do Just struct <- runGen structGen (show pid)
> return struct
>
> -- WORKS
> myGen' :: Gen String Struct -> GenDef Int [Struct]
> myGen' structGen =
> mkGen "myGen" $ \pid ->
> do pats <- getPatients
> let patToStruct pid =
> do Just struct <- runGen structGen (show pid)
> return struct
> structs <- mapM patToStruct pats
> return structs
>
> -- WORKS
> myGen'' :: Gen String Struct -> GenDef Int [Struct]
> myGen'' structGen =
> mkGen "myGen" $ \pid ->
> do pats <- getPatients
> structs <- mapM patToStruct pats
> return structs
> where
> patToStruct :: GenM m => Int -> m Struct
> patToStruct pid =
> do Just struct <- runGen structGen (show pid)
> return struct
>
> }}}
New description:
when using `RankNTypes` and `TypeFamilies` with polymorphic functions,
type inference works in let but not in where clauses.
{{{
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
import Control.Monad
class Monad m => GenM m where
type GenReq m :: *
type GenFun a b = forall m. GenM m => a -> m b
data GenDef a b = GenDef { name :: String, fun :: GenFun a b }
data Gen a b = Gen
data Struct = Struct
mkGen :: forall a b. String -> GenFun a b -> GenDef a b
mkGen = GenDef
runGen :: GenM m => Gen a b -> a -> m (Maybe b)
runGen = undefined
getPatients :: GenM m => m [Int]
getPatients = undefined
-- BROKEN
myGen :: Gen String Struct -> GenDef Int [Struct]
myGen structGen =
mkGen "myGen" $ \pid ->
do pats <- getPatients
structs <- mapM patToStruct pats
return structs
where
patToStruct pid =
do Just struct <- runGen structGen (show pid)
return struct
-- WORKS
myGen' :: Gen String Struct -> GenDef Int [Struct]
myGen' structGen =
mkGen "myGen" $ \pid ->
do pats <- getPatients
let patToStruct pid =
do Just struct <- runGen structGen (show pid)
return struct
structs <- mapM patToStruct pats
return structs
-- WORKS
myGen'' :: Gen String Struct -> GenDef Int [Struct]
myGen'' structGen =
mkGen "myGen" $ \pid ->
do pats <- getPatients
structs <- mapM patToStruct pats
return structs
where
patToStruct :: GenM m => Int -> m Struct
patToStruct pid =
do Just struct <- runGen structGen (show pid)
return struct
}}}
--
Comment:
Well, I'm afraid this is by design.
With `TypeFamilies`, local let or where bindings are not generalised; see
Section 4.2 of the
[http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn OutsideIn
paper]. So,
* In `myGen''` you give a type signature; and indeed `patToStruct` has
the type you specify.
* In `mkGen'` the `let` is not generalised, but it's fine because it's
only called at one type.
* In `mkGen`, the `where` is not generalised, and this time it does
matter, because the (monomorphic) `patToStruct` is outside the `(\pid ->
...)`, which itself is specified to have the polymorphic type `GenFun Int
[Struct]`. So there is a skolem-escape problem:
{{{
T7288.hs:30:28:
Couldn't match type `m0' with `m'
because type variable `m' would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: GenM m => Int -> m [Struct]
at T7288.hs:(28,5)-(31,25)
Expected type: Int -> m Struct
Actual type: Int -> m0 Struct
Relevant bindings include
patToStruct :: Int -> m0 Struct (bound at T7288.hs:33:11)
In the first argument of `mapM', namely `patToStruct'
In a stmt of a 'do' block: structs <- mapM patToStruct pats
In the expression:
do { pats <- getPatients;
structs <- mapM patToStruct pats;
return structs }
}}}
It's not a `let` vs `where` issue; the question is whether the non-
generalised binding is outside the expression with a forall'd type.
You can change the behaviour by adding `NoMonoLocalBinds` (after
`TypeFamilies`) as a LANGUAGE pragma. Then GHC tries harder, but less
robustly and predictably.
I wish I knew a better solution, but currently I don't.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7288#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
