[GHC] #14539: untouchable type inside the constraints

28 Nov 2017

      #14539: untouchable type inside the constraints
-------------------------------------+-------------------------------------
           Reporter:  Lemming        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code is taken and simplified from the test-suite of
 `accelerate-fourier`:
 {{{
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE Rank2Types #-}
 module UntouchableType (tests) where

 import Test.QuickCheck (Testable, Arbitrary, arbitrary, quickCheck, )

 newtype Sign a = Sign a
    deriving (Show)

 instance Arbitrary (Sign a) where
    arbitrary = undefined

 quickCheckWithSign :: (Testable prop) => (Sign Double -> prop) -> IO ()
 quickCheckWithSign = quickCheck

 data Array sh a = Array

 type family FullShape sh :: *

 data SubTransform a =
         SubTransform (forall sh. (FullShape sh ~ sh) => Array sh a)

 transform2d :: SubTransform Double -> Bool
 transform2d = undefined

 transformChirp2 :: Sign a -> Array sh a
 transformChirp2 = undefined

 tests :: IO ()
 tests =
    quickCheck $ \sign ->
       transform2d (SubTransform (transformChirp2 (sign::Sign Double)))
 }}}

 GHC-8.2.2 says about it:
 {{{
 [1 of 1] Compiling UntouchableType  ( UntouchableType.hs, interpreted )

 UntouchableType.hs:34:4: error:
     • Ambiguous type variable ‘p0’ arising from a use of ‘quickCheck’
       prevents the constraint ‘(Arbitrary p0)’ from being solved.
       Probable fix: use a type annotation to specify what ‘p0’ should be.
       These potential instances exist:
         instance (Arbitrary a, Arbitrary b) => Arbitrary (Either a b)
           -- Defined in ‘Test.QuickCheck.Arbitrary’
         instance Arbitrary Ordering
           -- Defined in ‘Test.QuickCheck.Arbitrary’
         instance Arbitrary Integer
           -- Defined in ‘Test.QuickCheck.Arbitrary’
         ...plus 20 others
         ...plus 62 instances involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the expression:
         quickCheck
           $ \ sign
               -> transform2d
                    (SubTransform (transformChirp2 (sign :: Sign Double)))
       In an equation for ‘tests’:
           tests
             = quickCheck
                 $ \ sign
                     -> transform2d
                          (SubTransform (transformChirp2 (sign :: Sign
 Double)))
    |
 34 |    quickCheck $ \sign ->
    |    ^^^^^^^^^^^^^^^^^^^^^...

 UntouchableType.hs:35:51: error:
     • Couldn't match expected type ‘Sign Double’ with actual type ‘p0’
         ‘p0’ is untouchable
           inside the constraints: FullShape sh ~ sh
           bound by a type expected by the context:
                      forall sh. FullShape sh ~ sh => Array sh Double
           at UntouchableType.hs:35:20-69
     • In the first argument of ‘transformChirp2’, namely
         ‘(sign :: Sign Double)’
       In the first argument of ‘SubTransform’, namely
         ‘(transformChirp2 (sign :: Sign Double))’
       In the first argument of ‘transform2d’, namely
         ‘(SubTransform (transformChirp2 (sign :: Sign Double)))’
     • Relevant bindings include
         sign :: p0 (bound at UntouchableType.hs:34:18)
    |
 35 |       transform2d (SubTransform (transformChirp2 (sign::Sign
 Double)))
    |                                                   ^^^^
 Failed, no modules loaded.
 }}}
 I have tested GHC versions back to GHC-7.4.2, all of them report
 essentially the same type error.

 I do not really understand the type error message, but here are my
 observations that I find strange:
 The type annotation `sign :: Sign Double` does not prevent the type error,
 but replacing `quickCheck` by `quickCheckWithSign` does.
 Replacing the constraint `FullShape sh ~ sh` by, e.g. `Show sh`, let the
 error disappear.
 Generalizing `transform2d` to `SubTransform a` causes another type error
 although I expected that `SubTransform Double` can be infered from `Sign
 Double`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14539
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler