Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#7288 closed bug (invalid)

type inference fails with where clause (RankNTypes, TypeFamilies)

Reported by: agrafix Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.1
Keywords: type inference, rankntypes, typefamilies Cc: leuschner@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by simonpj)

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

Change History (3)

comment:1 Changed 2 years ago by dleuschner

  • Cc leuschner@… added

comment:2 follow-up: Changed 2 years ago by simonpj

  • Description modified (diff)
  • difficulty set to Unknown
  • Resolution set to invalid
  • Status changed from new to closed

Well, I'm afraid this is by design.

With TypeFamilies, local let or where bindings are not generalised; see Section 4.2 of the 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.

comment:3 in reply to: ↑ 2 Changed 2 years ago by dleuschner

Thanks, Simon! I guess it looked like it was a let vs. where issue because the indentation suggests that the where-clause is inside the scope of the lambda but it isn't. It would be nice if lambdas could have where bindings. :-)

Replying to simonpj:

Well, I'm afraid this is by design.

With TypeFamilies, local let or where bindings are not generalised; see Section 4.2 of the 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.

Note: See TracTickets for help on using tickets.