Opened 2 years ago

Last modified 2 years ago

#14132 new feature request

Report an error for a missing class instance before an error for type family instances of an associated type.

Reported by: duog Owned by: duog
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following code

{-# LANGUAGE FlexibleContexts, TypeFamilies, DataKinds #-}

import GHC.Generics
import GHC.TypeLits

type family RepHasNoInstance (f :: * -> *) ::  *

-- edit 1
-- type instance RepHasNoInstance f = Int

-- edit 2
-- class RepHasNoInstanceC (f :: * -> *)
-- foo :: (Generic a, RepHasNoInstanceC (Rep a)) => a -> Int
-- foo = const 1
foo :: (Generic a, RepHasNoInstance (Rep a) ~ Int) => a -> Int
foo = const 1

data NotGeneric = NotGeneric

bar :: NotGeneric -> Int
bar = foo

main :: IO ()
main = return ()

gives an error like

associated-type-families-test.hs:21:7: error:
    • Couldn't match type ‘RepHasNoInstance (Rep NotGeneric)’
                     with ‘Int’
        arising from a use of ‘foo’
    • In the expression: foo
      In an equation for ‘bar’: bar = foo
   |
21 | bar = foo
   |       ^^^

in ghcs: 8.0.2, 8.2.1, master(a few days old).

The error message is for ambiguous types in 7.10.3

Uncommenting edit 1, the error changes to:

associated-type-families-test.hs:16:7: error:
    • No instance for (Generic NotGeneric) arising from a use of ‘foo’
    • In the expression: foo
      In an equation for ‘bar’: bar = foo
   |
16 | bar = foo
   | 

I think this is a much better error message, since there is no hope for the associated type to have an instance for anything unless there is an instance (Generic NotGeneric).

Uncommenting edit 2, (and commenting the existing foo) gives the "No instance for (Generic NotGeneric)" message.

Attachments (1)

T12170a.comp.stderr (6.2 KB) - added by duog 2 years ago.

Download all attachments as: .zip

Change History (8)

comment:1 Changed 2 years ago by simonpj

Yes, I think it'd be possible to improve this. At the moment we actually suppress the class error because of the type-equality error. But with a little re-ordering in TcErrors.reportWanteds we could fix that. Then we'd at least report both. Suppressing the equality error because it involves an associated type would be significantly harder. But at least you'd get both.

Specifically the code in TcErrors is this

    report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
              , given_eq_spec
              , ("insoluble2",    utterly_wrong,    True, mkGroupReporter mkEqErr)
              , ("skolem eq1",    very_wrong,       True, mkSkolReporter)
              , ("skolem eq2",    skolem_eq,        True, mkSkolReporter)
              , ("non-tv eq",     non_tv_eq,        True, mkSkolReporter)
              , ("Out of scope",  is_out_of_scope,  True, mkHoleReporter)
              , ("Holes",         is_hole,          False, mkHoleReporter)

                  -- The only remaining equalities are alpha ~ ty,
                  -- where alpha is untouchable; and representational equalities
                  -- Prefer homogeneous equalities over hetero, because the
                  -- former might be holding up the latter.
                  -- See Note [Equalities with incompatible kinds] in TcCanonical
              , ("Homo eqs",      is_homo_equality, True,  mkGroupReporter mkEqErr)
              , ("Other eqs",     is_equality,      False, mkGroupReporter mkEqErr) ]

    -- report2: we suppress these if there are insolubles elsewhere in the tree
    report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)
              , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)
              , ("Dicts",           is_dict,         False, mkGroupReporter mkDictErr) ]

I think that moving the "non-tv-eq" line from report1 into report2 would do the job. (And maybe change that True to False.)

The "Homo eqs" and "Other eqs" could move too.

I'm swamped right now, and this would make lots of error messages in validate change slightly, each of which needs a check and accept. But maybe someone else can have a go?

comment:2 Changed 2 years ago by duog

Owner: set to duog

I will have a go

comment:3 Changed 2 years ago by duog

I had a go at this yesterday, but I ran into a problem. There is a comment on report1:

    -- report1: ones that should *not* be suppresed by
    --          an insoluble somewhere else in the tree
    -- It's crucial that anything that is considered insoluble
    -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
    -- we might suppress its error message, and proceed on past
    -- type checking to get a Lint error later

This means moving ReporterSpecs between report1 and report2 doesn't work as is. It would be possible to make it work by adding some complexity to the suppression logic; make ReporterSpecs in report2 unable to suppress ReporterSpecs in report1.

Alternatively, I think I see how to suppress the equality error in favour of the class instance error:

The tuples in report1 and report2 are of type ReporterSpec:

type Reporter
  = ReportErrCtxt -> [Ct] -> TcM ()
type ReporterSpec
  = ( String                     -- Name
    , Ct -> PredTree -> Bool     -- Pick these ones
    , Bool                       -- True <=> suppress subsequent reporters
    , Reporter)                  -- The reporter itself

In tryReporter, the current list of unsatisfiable constraints is partitioned with the 2nd member of the tuple. The matching constraints are passed to the Reporter, and the non-matching constraints are returned for the next iteration of tryReporter.

I propose to change the definition to:

type Reporter
  = ReportErrCtxt -> [Ct] -> TcM [Ct]
type ReporterSpec
  = ( String                     -- Name
    , Bool                       -- True <=> suppress subsequent reporters
    , Reporter)                  -- The reporter itself

Now the partitioning will be done inside the Reporter, and we can write something like:

associated_type_eq :: Reporter
associated_type_eq ctxt cts = 
  let associated_type_cts = 
        [ (tf_ct, dict_cts)
        | tf_ct <- cts
        , EqPred NomEq ty1 _ <- [classifyPredType (ctPred ct)]  
        , (FamilyTyCon{famTcParent = Just cls}, tf_tys) <- ["some function 1" ty1]
        , let dict_cts =
                [ ct'
                | ct' <- cts
                , ClassPred cls' cls_tys <- [classifyPredType (ctPred ct)]
                , cls' == cls && tf_tys "some function 2" cls_tys
                ]
        ]
      yeses = [x 
              | (tf_ct, dict_cts) <- associated_type_cts
              , x <- tf_ct : dict_cts
              ]
      noes = filter (`notElem` yeses) cts
  in do
    mkGroupReporter mkDictErr ctxt $ 
      concat [dict_cts | (_, dict_cts) <- associated_type_cts]
    return noes

where "some function 1" gives the type constructor and it's arguments, and "some function 2" checks that this associated type comes from this instance. These functions must exist right?

Do you know of any other cases that could be improved by this more powerful factoring?

This would affect tracing, since currently in tryReporter the partitioning is done, and if the predicate matches anything tryReporter traces the Cts that matched. With the partitioning inside the Reporter this doesn't work anymore. Perhaps the Reporter could also return the yeses.

Please let me know whether you think this is a good idea, otherwise I will go ahead and do the simpler option of adding some complexity to the suppression logic.

comment:4 Changed 2 years ago by simonpj

This means moving ReporterSpecs between report1 and report2 doesn't work as is

I don't agree. I believe you can move "non-tv-eqs", "homo-eqs" and "otehr-eqs"; they are not "truly insoluble".

Ah: I see that trulyInsoluble is a poorly-named predicate. It is only applied to constraints in wc_insol, and they are things like Int ~ Bool, but NOT things like a ~ Int (which are no necessarily insoluble). It'd be much clearer if trulyInsoluble really did check for truly-insoluble constraints.

Separately I'd been thinking that separating wc_insol from wc_simple is a waste of effort; it'd be better to combine them.

Changed 2 years ago by duog

Attachment: T12170a.comp.stderr added

comment:5 Changed 2 years ago by duog

I tried moving those three ReporterSpecs to report2 (keeping their order, just adding them after "Dicts") and T12170a gave a core lint error (attached). I had assumed it was due to the invariant specified in the comment.

I am obviously very new to the typechecker; my presumption was that insoluble constraints were ones that we couldn't defer by inserting a coercion, so it would be very bad to suppress those errors. That was my untrained reading of the lint error. However this must be wrong, because surely there's no problem inserting a coercion from Int to Bool.

comment:6 Changed 2 years ago by simonpj

Ah. That turned out to be a separate bug: #14149. I'll commit a fix for it shortly.

comment:7 Changed 2 years ago by simonpj

OK #14149 is fixed, so you can have another go.

Note: See TracTickets for help on using tickets.