Skip to content

GHC behaves differently when binding has separate or inlined type declaration

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main = do
    let a :: forall t. Functor t => t () = undefined
    let g :: forall u. Functor u => u () = a
    putStrLn "success"

fails with:

source_file.hs:6:44:
    Couldn't match expected type ‘forall (u :: * -> *).
                                  Functor u =>
                                  u ()’
                with actual type ‘t0 ()’
    When checking that: t0 ()
      is more polymorphic than: forall (u :: * -> *). Functor u => u ()
    In the expression: a

but the following compiles successfully

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

main = do
    let a :: forall t. Functor t => t () = undefined
    let g :: forall u. Functor u => u ()
        g = a
    putStrLn "success"

On GHC 7.10 it works as described above. On 8.4.4 it fails even on the "functioning code".

a.hs:5:44: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls:
        forall (t :: * -> *). Functor t => t ()
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In a pattern binding:
        a :: forall (t :: * -> *). Functor t => t () = undefined
      In the expression:
        do let a :: forall t. Functor t => t () = undefined
           let g :: forall u. Functor u => u ()
               g = a
           putStrLn "success"
Edited by fghibellini
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information