[GHC] #13775: Type family expansion is too lazy, allows accepting of ill-typed terms

[GHC]

#13775: Type family expansion is too lazy, allows accepting of ill-typed terms
-------------------------------------+-------------------------------------
        Reporter:  fizruk            |                Owner:  diatchki
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |             Keywords:
      Resolution:                    |  CustomTypeErrors
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 I think that this is more a question about how type functions work, rather
 than `TypeError` specifically.

 Currently, GHC does not evaluate type functions unless it needs to, so
 there is no error reported.  Similarly, GHC does not report any errors for
 the following example,
 which has nothing to do with `TypeError`:

 {{{
 type family F a

 test = show (Proxy @ (Proxy (F Int))
 }}}

 This works just fine and prints `Proxy`, it does not report a missing
 instance for `F Int`.   I don't really like this behavior of GHC, but
 that's an orthogonal issue.

 I am not sure how I could be more aggressive with `TypeError` without a
 bunch of special cases, and also, last time we discussed this people
 seemed to want the lazy behavior.

 I'll take on updating the manual to be more explicit about the behavior.

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