Opened 2 years ago

Last modified 14 months ago

#13775 new bug

Type family expansion is too lazy, allows accepting of ill-typed terms

Reported by: fizruk Owned by: diatchki
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.2
Keywords: CustomTypeErrors Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I'm using GHC 8.0.2 and I've just witnessed a weird bug.

To reproduce a bug I use this type family, using TypeError (this is a minimal type family I could get to keep bug reproducible):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

type family Head xs where
  Head '[] = TypeError (Text "empty list")
  Head (x ': xs) = x

Then I go to GHCi, load this code and observe this:

>>> show (Proxy @ (Head '[]))
"Proxy"

This looks like a bug to me! I expect Head '[] to produce a type error. And indeed it does, if I ask differently:

>>> Proxy @ (Head '[])

<interactive>:9:1: error:
    • empty list
    • When checking the inferred type
        it :: Proxy (TypeError ...)

So far it looks like show somehow "lazily" evaluates it's argument type and that's why it's possible to show Proxy even when Proxy is ill-typed.

But if I expand Head '[] manually then it all works as expected again:

>>> show $ Proxy @ (TypeError (Text "error"))

<interactive>:13:8: error:
    • error
    • In the second argument of ‘($)’, namely
        ‘Proxy @(TypeError (Text "error"))’
      In the expression: show $ Proxy @(TypeError (Text "error"))
      In an equation for ‘it’:
          it = show $ Proxy @(TypeError (Text "error"))

You can remove TypeError from the original type family:

type family Head xs where
  Head (x ': xs) = x

And it gets even weirder:

>>> show (Proxy @ (Head '[]))
"Proxy"
>>> Proxy @ (Head '[])
Proxy

I did not test this with GHC 8.2.

I think this behaviour is not critical for me, but accepting ill-typed terms looks like a bad sign, especially for type-level-heavy programs.

Change History (10)

comment:1 Changed 2 years ago by RyanGlScott

Architecture: x86_64 (amd64)Unknown/Multiple
Keywords: CustomTypeErrors added
Operating System: MacOS XUnknown/Multiple

Also reproducible in GHC 8.2 and HEAD.

comment:2 Changed 2 years ago by fizruk

By the way, if you mistype Proxy as Prox, you can also get GHC panic:

>>> Prox @ (Head '[])
ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.2 for x86_64-apple-darwin):
	initTc: unsolved constraints
  WC {wc_insol =
        [W] Prox_a1L4 :: t_a1L3[tau:1] (CHoleCan: Prox)
        [W] Prox_a1Ls :: t_a1Lr[tau:1] (CHoleCan: Prox)}

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

But this panic seems to be because of TypeApplications and can be reproduced with just two lines in GHCi:

>>> :set -XTypeApplications
>>> X @ Int
ghc: panic! (the 'impossible' happened)
  (GHC version 8.0.2 for x86_64-apple-darwin):
	initTc: unsolved constraints
  WC {wc_insol =
        [W] X_a13x :: t_a13w[tau:1] (CHoleCan: X)
        [W] X_a13V :: t_a13U[tau:1] (CHoleCan: X)}

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Should I file this one separately?

comment:3 Changed 2 years ago by RyanGlScott

That one is actually a known bug (#13466) which has been fixed in GHC 8.2.1.

comment:4 Changed 2 years ago by simonpj

Owner: set to diatchki

This is really a question for Iavor, who implemented user-specified type errors. The user manual section on custom errors does not explain the behaviour of the feature (except with a single example), and need some serious love.

What is happening is this:

  • GHC only reports custom type errors if
    • We have an unsolved constraint involving TypeError
    • We have a declared or inferred type involving TypeError
  • We get a constraint Show (Proxy (TypeError "...")).
  • But the instance for Proxy is
    instance Show (Proxy s) where ...
    
    so the TypeError... is discarded.
  • All constraints are solved, so no error is reported.

Iavor: you may want to consider being more aggressive? Or at least documenting the expected behaviour better. Thanks!

comment:5 Changed 2 years ago 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.

comment:6 Changed 2 years ago by simonpj

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

No, I don't think it is. GHC never reports an error simply becuase it tries to evaluate TypeError ... Rather, that call is stuck. That in turn may mean that some constraint can't be solved. And then, when reporting unsolved constraints, GHC looks for any nested calls to TypeError and reports them rather than the constraint itself. You wrote this code!

It's nothing to do with how much reduction takes place, IMHO.

comment:7 Changed 2 years ago by diatchki

I remember how the implementation works.

My comment was about the fact that GHC is perfectly happy to treat "stuck" types as ordinary types without fully resolving them, which is why it can solve constraints such as Show (Proxy (TypeError ...)), or Show (Proxy (F Int)).

A different design choice is to refuse to solve such constraints until GHC is sure that the type functions involved will produce a valid result, but that's not what we currently do. As a result, neither the TypeError nor the missing F Int instance are reported, and the Show constraint is happily solved, which is---perhaps---somewhat confusing.

comment:8 Changed 2 years ago by simonpj

Sorry -- I didn't mean to sound snarky!

A different design choice is to refuse to solve such constraints until GHC is sure that the type functions involved will produce a valid result

I think you are suggesting that

  • Don't do any work on a constraint that mentions TypeError. E.g. C [TypeError ..] would never be solved, regardless of the instances for C.

That sounds attractive, but it's fragile. Suppose we had [W] C [alpha] where alpha is a unification variable. Can we use an instance declaration on that? Well, no; it might turn out that, after hundreds more simplification steps on other constraints mentioning alpha, that alpha := TypeError....

Or it might be [W] C (F alpha), where eventually alpha := Int, and then we reduce F Int to TypeError....

So I don't see how to make this approach robustly implementable.

comment:9 Changed 14 months ago by tom-bop

Are we sure this has to do with TypeErrors? I see the same problem without them:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

type family Head xs where
  -- As written, this compiles, and it also compiles if you uncomment either
  --   of these lines:

  -- Head '[] = 'True ~ 'False
  -- Head '[] = TypeError ('Text "empty list")

  Head (x ': xs) = x

main = print $ show (Proxy::Proxy (Head '[]))

comment:10 Changed 14 months ago by simonpj

Well we hvae

instance Show (Proxy s) where ...

Notice that s is not used. So the instance will work just fine if s = Head '[].

I don't regard this as a bug (yet, anyway). It accepts more programs than at least some people expect; but well typed programs (ones that are accepted) don't go wrong at runtime, which is what we ask from our type system.

Note: See TracTickets for help on using tickets.