[GHC] #14771: TypeError reported too eagerly

[GHC]

#14771: TypeError reported too eagerly
-------------------------------------+-------------------------------------
           Reporter:  hsyl20         |             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:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following example:
 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}

 import GHC.TypeLits
 import Data.Proxy

 data DUMMY

 type family If c t e where
    If True t e  = t
    If False t e = e


 type family F (n :: Nat) where
    --F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
    F n = If (n <=? 8) Int DUMMY

 test :: (F n ~ Word) => Proxy n -> Int
 test _ = 2

 test2 :: Proxy (n :: Nat) -> Int
 test2 p = test p

 main :: IO ()
 main = do
    print (test2 (Proxy :: Proxy 5))
 }}}

 The type error is useful:
 {{{
 Bug.hs:26:11: error:
     • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
         arising from a use of ‘test’
     • In the expression: test p
       In an equation for ‘test2’: test2 p = test p
     • Relevant bindings include
         p :: Proxy n (bound at Bug.hs:26:7)
         test2 :: Proxy n -> Int (bound at Bug.hs:26:1)
    |
 26 | test2 p = test p
    |           ^^^^^^
 }}}

 Now if we use the commented implementation of `F` (using `TypeError`),
 with GHC 8.2.2 and 8.0.2 we get:
 {{{
 Bug.hs:26:11: error:
     • ERROR
     • In the expression: test p
       In an equation for ‘test2’: test2 p = test p
    |
 26 | test2 p = test p
    |           ^^^^^^
 }}}

 While with GHC 8.0.1 we get:
 {{{
 /home/hsyl20/tmp/Bug.hs:29:11: error:
     • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
                      with ‘Word’
         arising from a use of ‘test’
     • In the expression: test p
       In an equation for ‘test2’: test2 p = test p
 }}}

 1) Could we restore the behavior of GHC 8.0.1?

 2) In my real code, when I use DUMMY I get:
 {{{
     • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
       Expected type: Word
         Actual type: F n
 }}}
 If we could get the same report (mentioning the "Actual type") when we use
 `TypeError` that would be great.

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