[GHC] #7288: type inference fails with where clause (RankNTypes, TypeFamilies)

[GHC]

#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