[GHC] #14319: Stuck type families can lead to lousy error messages (was: Stuck kind families can lead to lousy error messages)

[GHC]

#14319: Stuck type families can lead to lousy error messages
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.3
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by dfeuer:

Old description:

> {{{#!hs
> {-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}
>
> module ArityError where
> import Data.Kind
> import GHC.TypeLits
> import Data.Proxy
>
> type family F (s :: Symbol) :: Type
> type family G (s :: Symbol) :: F s
> type instance G "Hi" = Maybe
> }}}
>
> This produces the error message
>
> {{{#!hs
> ArityError.hs:10:24: error:
>     • Expecting one more argument to ‘Maybe’
>       Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* -> *’
>     • In the type ‘Maybe’
>       In the type instance declaration for ‘G’
>    |
> 10 | type instance G "Hi" = Maybe
>    |                        ^^^^^
> }}}
>
> This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what
> arity it indicates. What I ''think'' is a term level version of this,
>
> {{{#!hs
> f :: forall (s :: Symbol). Proxy s -> F s
> f _ = Just
> }}}
>
> gives a much less confusing message:
>
> {{{
> ArityError.hs:14:7: error:
>     • Couldn't match expected type ‘F s’
>                   with actual type ‘a0 -> Maybe a0’
>       The type variable ‘a0’ is ambiguous
>     • In the expression: Just
>       In an equation for ‘f’: f _ = Just
>     • Relevant bindings include
>         f :: Proxy s -> F s (bound at ArityError.hs:14:1)
>    |
> 14 | f _ = Just
>    |       ^^^^
> }}}
>
> The fix (I think) is to refrain from reporting arity errors when we don't
> know enough about the relevant arities.

New description:

 I first noticed this problem at the type level:

 {{{#!hs
 {-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}

 module ArityError where
 import Data.Kind
 import GHC.TypeLits
 import Data.Proxy

 type family F (s :: Symbol) :: Type
 type family G (s :: Symbol) :: F s
 type instance G "Hi" = Maybe
 }}}

 This produces the error message

 {{{#!hs
 ArityError.hs:10:24: error:
     • Expecting one more argument to ‘Maybe’
       Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* -> *’
     • In the type ‘Maybe’
       In the type instance declaration for ‘G’
    |
 10 | type instance G "Hi" = Maybe
    |                        ^^^^^
 }}}

 This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity
 it indicates.

 ----

 I just realized we have a similar problem at the term level:

 {{{#!hs
 f :: forall (s :: Symbol). Proxy s -> F s
 f _ _ = undefined
 }}}

 produces

 {{{#!hs
 ArityError.hs:14:1: error:
     • Couldn't match expected type ‘F s’ with actual type ‘p0 -> a0’
       The type variables ‘p0’, ‘a0’ are ambiguous
     • The equation(s) for ‘f’ have two arguments,
       but its type ‘Proxy s -> F s’ has only one
     • Relevant bindings include
         f :: Proxy s -> F s (bound at ArityError.hs:14:1)
    |
 14 | f _ _ = undefined
    | ^^^^^^^^^^^^^^^^^
 }}}

 The claim that `Proxy s -> F s` has only one argument is bogus; we only
 know that it has ''at least'' one argument. The fix (I imagine) is to
 refrain from reporting arity errors when we don't know enough about the
 relevant arities.

--

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