Type checker regression introduced by visible type-application

TODO: figure out better summary ;-)

The following snippet extracted from Edward's profunctors package compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Data.Profunctor.Strong where

import Control.Arrow
import Control.Category
import Data.Tuple
import Prelude hiding (id,(.))

infixr 0 :->
type p :-> q = forall a b. p a b -> q a b

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

class ProfunctorFunctor t where
  promap    :: Profunctor p => (p :-> q) -> t p :-> t q

class ProfunctorFunctor t => ProfunctorMonad t where
  proreturn :: Profunctor p => p       :-> t p
  projoin   :: Profunctor p => t (t p) :-> t p

class ProfunctorFunctor t => ProfunctorComonad t where
  proextract   :: Profunctor p => t p :-> p
  produplicate :: Profunctor p => t p :-> t (t p)

class Profunctor p => Strong p where
  first' :: p a b  -> p (a, c) (b, c)
  first' = dimap swap swap . second'

  second' :: p a b -> p (c, a) (c, b)
  second' = dimap swap swap . first'

----------------------------------------------------------------------------

newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }

instance Profunctor p => Profunctor (Tambara p) where
  dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p

instance ProfunctorFunctor Tambara where
  promap f (Tambara p) = Tambara (f p)

instance ProfunctorComonad Tambara where
  proextract (Tambara p) = dimap (\a -> (a,())) fst p

  produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
    where
      hither :: ((a, b), c) -> (a, (b, c))
      hither ~(~(x,y),z) = (x,(y,z))

      yon    :: (a, (b, c)) -> ((a, b), c)
      yon    ~(x,~(y,z)) = ((x,y),z)

instance Profunctor p => Strong (Tambara p) where
  first' = runTambara . produplicate

Strong.hs:57:12: error:
    • Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1. Tambara p (a, c1) (b, c1)’
      Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)
        Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c) (b, c)
    • In the first argument of ‘(.)’, namely ‘runTambara’
      In the expression: runTambara . produplicate
      In an equation for ‘first'’: first' = runTambara . produplicate
    • Relevant bindings include first' :: Tambara p a b -> Tambara p (a, c) (b, c) (bound at Strong.hs:57:3)

Trac metadata

Trac field	Value
Version	7.11
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	alanz
Operating system
Architecture