[GHC] #15772: Strange constraint error that disappears when adding another top-level declaration

18 Oct 2018

      #15772: Strange constraint error that disappears when adding another top-level
declaration
-------------------------------------+-------------------------------------
           Reporter:  kosmikus       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.1
  (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:
-------------------------------------+-------------------------------------
 Consider this program:
 {{{#!hs
 {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances
 #-}
 module CURepro where

 import Data.Kind

 data NP (f :: Type -> Type) (xs :: [Type])

 type family Curry (f :: Type -> Type) (xs :: [Type]) (r :: Type) (a ::
 Type) :: Constraint where
   Curry f xs r (f x -> a) = (xs ~ (x : Tail xs), Curry f (Tail xs) r a)
   Curry f xs r a          = (xs ~ '[], r ~ a)

 type family Tail (a :: [Type]) :: [Type] where
   Tail (_ : xs) = xs

 uncurry_NP :: (Curry f xs r a) => (NP f xs -> r) -> a
 uncurry_NP = undefined

 fun_NP :: NP Id xs -> ()
 fun_NP = undefined

 newtype Id a = MkId a

 -- test1 :: ()
 -- test1 = uncurry_NP fun_NP (MkId 5)

 test2 :: ()
 test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
 }}}

 With GHC 8.6.1 (and also 8.4.3), this produces the following error
 message:
 {{{
 CURepro.hs:27:9: error:
     • Couldn't match type ‘Tail t0’ with ‘Bool : Tail (Tail t0)’
         arising from a use of ‘uncurry_NP’
       The type variable ‘t0’ is ambiguous
     • In the expression:
         uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
       In an equation for ‘test2’:
           test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
    |
 27 | test2 = uncurry_NP fun_NP (MkId True) (MkId 5) (MkId True)
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 However, uncommenting the definition of `test1` makes the whole program
 check without error!

 I think both versions of the program should be accepted.

 I've tried to extract this from a much larger failing example, but did not
 manage to make it any smaller than this. In particular, the fact that `NP`
 is parameterised over a type constructor `f` seems to be somehow essential
 to trigger this.

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