Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#9582 closed bug (fixed)

Associated Type Synonyms do not unfold in InstanceSigs

Reported by: andreas.abel Owned by:
Priority: normal Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.8.3
Keywords: InstanceSigs TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T9582
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# LANGUAGE InstanceSigs, TypeFamilies #-}

class C a where
  type T a
  m :: T a

instance C Int where
  type T Int = String
  m :: String
  m = "bla"

-- Method signature does not match class; it should be m :: T Int
--    In the instance declaration for ‘C Int’

As T Int is a synonym of String, m :: String should be a valid type signature alternative to m :: T Int

Change History (14)

comment:1 Changed 5 years ago by andreas.abel

Relevant snippet: Checking InstanceSigs uses eqType.

https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcInstDcls.lhs

    -- Check that any type signatures have exactly the right type
    check_inst_sig hs_ty@(L loc _)
       = setSrcSpan loc $
         do { sig_ty <- tcHsSigType (FunSigCtxt sel_name) hs_ty
            ; inst_sigs <- xoptM Opt_InstanceSigs
            ; if inst_sigs then
                unless (sig_ty `eqType` local_meth_ty)
                       (badInstSigErr sel_name local_meth_ty)
              else
                addErrTc (misplacedInstSig sel_name hs_ty)
            ; return sig_ty }

Last commit: https://github.com/ghc/ghc/commit/7fa2ce2043e2faed2b2b545ba5c1c9958954800a

According to the documentation, eqType only takes type synonyms into account (not type families).

https://github.com/ghc/ghc/blob/master/compiler/types/Type.lhs

eqType :: Type -> Type -> Bool
-- ^ Type equality on source types. Does not look through @newtypes@ or
-- 'PredType's, but it does look through type synonyms.
-- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
eqType t1 t2 = isEqual $ cmpType t1 t2

cmpType :: Type -> Type -> Ordering
-- Watch out for horrible hack: See Note [Comparison with OpenTypeKind]
cmpType t1 t2 = cmpTypeX rn_env t1 t2
  where
    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))

cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
cmpTypeX env t1 t2 | Just t1' <- coreView t1 = cmpTypeX env t1' t2
                   | Just t2' <- coreView t2 = cmpTypeX env t1 t2'
-- We expand predicate types, because in Core-land we have
-- lots of definitions like
--      fOrdBool :: Ord Bool
--      fOrdBool = D:Ord .. .. ..
-- So the RHS has a data type

cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
-- plus congruences...

Where to find the type equality check that honors type family instances?

comment:2 Changed 5 years ago by simonpj

It's not just type families. You'd also expect that re-ordering the constraints in a qualified context would make no difference:

expected:   (Eq a, Num a) => a -> a
actual:     (Num a, Eq a) => a -> a

I think the Right Thing is to use TcUnify.tcSubType, twice. It checks that t1 is more polymorphic than t2; so you can call it with t1,t2 and with t2,t1. It instantiates one type, skolemises the other, and does full constraint solving. Look at other calls to tcSubType to see how it is used.

Simon

comment:3 Changed 5 years ago by andreas.abel

Thanks, Simon, I got quite far with your help:

    -- Check that any type signatures have exactly the right type
    check_inst_sig hs_ty@(L loc _)
       = setSrcSpan loc $
         do { let userTypeCtxt = FunSigCtxt sel_name
            ; sig_ty <- tcHsSigType userTypeCtxt hs_ty
            ; inst_sigs <- xoptM Opt_InstanceSigs
            ; if inst_sigs then do
                -- Check that type provided in the type signature
                -- is both a sub- and a super-type of the type
                -- originating from the method signature in the class.
                -- As a consequence, the types are equal, and we can discard
                -- the coercions.  (Keep fingers crossed.)
                let ctOrigin = AmbigOrigin userTypeCtxt
                void $ tcSubType ctOrigin userTypeCtxt sig_ty local_meth_ty
                (errMsgs, result) <- tryTcErrs $
                       tcSubType ctOrigin userTypeCtxt local_meth_ty sig_ty
                -- In case the provided type is more general than the expected
                -- type, we give a custom error message.
                -- Really, providing a method implementation of a more general type
                -- OUGHT to be allowed, so the error coming from a failure of subtyping
                -- is confusing.
                -- However, in the latter case we cannot simply discard the coercion...
                case result of
                  Just _coercion -> return ()
                  Nothing -> badInstSigErr sel_name local_meth_ty
                -- unless (sig_ty `eqType` local_meth_ty)
                --        (badInstSigErr sel_name local_meth_ty)
              else
                addErrTc (misplacedInstSig sel_name hs_ty)
            ; return sig_ty }

My test case is now accepted. I am also happy with the error message if the instance signature is too specific (first tcSubType check). I tried to give a better error message than the one thrown by tcSubTyp if the instance signature is more general than the method signature coming from the class. However, it does not seem to work, it is as if the tryTcErrs would not catch the errors thrown by tcSubType. This is unlikely however, my suspicion is that tcSubType just generates constraints which it hopes to solve later and then fails.

Anyway, I need some advice how to catch errors or replace errors by other ones...

For illustration, here is the case that the user gives a too general instance signature and receives a misleading error message:

{-# LANGUAGE InstanceSigs, TypeFamilies #-}

module Fail where

class C a where
  type T a
  m :: T a

instance C Int where
  type T Int = String

  -- The following type signature for m is currently rejected,
  -- as it is too general.
  m :: Show a => [a]
  m = []
    Couldn't match type ‘[Char]’ with ‘forall a. Show a => [a]’
    Expected type: forall a. Show a => [a]
      Actual type: T Int
    In the instance declaration for ‘C Int’

The error is confusing, at least because the roles of expected and actual types are reversed.

comment:5 Changed 5 years ago by thomie

Status: newpatch

comment:6 Changed 5 years ago by simonpj

I'm sorry about being slow to reply -- utterly swamped.

  1. 'tcSubType' does not generate errors, just postponed

constraints, which are checked later in a clean-up phase. Thus, I do not get an error now I could handle, but the error is generated later during the constraint solving phase, where I do not have a handler in place.

This is dead right, and I think it's a huge strength of GHC's current type inference mechanism. Essentially all type error messages are generated in TcErrors, not in places scattered over the compiler. This is not a "clean-up phase". It is the place that type errors are generated.

For tcSubType, the way to control your error messages is through the CtOrigin and UserTypeCtxt passed to tcSubType.

The UserTypeCtxt is attached (via the ic_info field of Implication) to the implication constraint generated by the tcSubType. If you want, you can add an extra constructor to UserTypeCtxt.

The CtOrigin is attached to the instantiated constraints generated by the sub-type check.

Both are accessible to the error-message generation in TcErrors.

In short, instead of catching the error(s) now, GHC just attaches enough information to the constraints that you can generate a good error message later.

I hope that is of some help.

Simon

comment:7 Changed 5 years ago by andreas.abel

Thanks for the help!

Now I use PatSigOrigin to swap expected/actual type in the error message generated by tcSubType.

                -- Check that type provided in the type signature
                -- is both a sub- and a super-type of the type
                -- originating from the method signature in the class.
                -- As a consequence, the types are equal, and we can discard
                -- the coercions.  (Keep fingers crossed.)
                let ctOrigin = AmbigOrigin userTypeCtxt
                void $ tcSubType ctOrigin userTypeCtxt sig_ty local_meth_ty
                -- In case the provided type is more general than the expected
                -- type, we take care that the error reports actual and
                -- expected type correctly.
                -- Using PatSigOrigin does the job, but it is a bit hacky.
                void $ tcSubType PatSigOrigin userTypeCtxt local_meth_ty sig_ty

This does the job, however, is a bit hacky. I tried a more principled solution with TypeEqOrigin,

               let ctOrigin' = TypeEqOrigin
                      { uo_actual   = sig_ty
                      , uo_expected = local_meth_ty
                      }
                void $ tcSubType ctOrigin' userTypeCtxt local_meth_ty sig_ty

but except for PatSigOrigin, instances of CtOrigin are ignore in tcSubType, or rather, converted to a standard TypeEqOrigin (with expected/actual ordered not in the way I want to). See TcUnify.lhs:

tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- Check that ty_actual is more polymorphic than ty_expected
-- Both arguments might be polytypes, so we must instantiate and skolemise
-- Returns a wrapper of shape   ty_actual ~ ty_expected
tcSubType origin ctxt ty_actual ty_expected

...  unify ty_actual ty_expected ...

  where
    -- In the case of patterns we call tcSubType with (expected, actual)
    -- rather than (actual, expected).   To get error messages the
    -- right way round we have to fiddle with the origin
    unify ty1 ty2 = uType u_origin ty1 ty2
      where
         u_origin = case origin of
                      PatSigOrigin -> TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 }
                      _other       -> TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }

This could be changed of course, bit there is a principal risk of breaking something. In particular, would it not make sense to preserve TypeEqOrigin?

                      TypeEqOrigin{} -> origin

If you give your OK, I implement this to make my fix of #9582 cleaner.

Working fix on https://github.com/andreasabel/ghc/commit/29a2f93a26f714b79a59617d20b73b2e166cc62c some cleaning needed.

Last edited 5 years ago by andreas.abel (previous) (diff)

comment:8 Changed 5 years ago by simonpj

The hack is horrible!

I suggest instead replacing the CtOrigin arg to tcSubPat with BasicTypes.SwapFlag. If NotSwapped then ty1 is acutal, ty2 is expected; if Swapped then the other way round.

That would make all the other calls more perspicuous too.

Simon

comment:9 Changed 5 years ago by andreas.abel

Agreed on the horror of the hack! I implemented your suggestion to change the interface of tcSubType, see: https://github.com/andreasabel/ghc/commit/e43d6f1f90f8d395fb21696c5f8a1641a75067b5 Instead of CtOrigin, it takes a SwapFlag. Note that it has to pass an origin to deeplyInstantiate, and as the original origin is no more communicated to tcSubType, it uses a standard TypeEqOrigin now. Whether this has any negative impact is yours to judge...

tcSubType :: SwapFlag -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- Check that ty_actual is more polymorphic than ty_expected
-- Both arguments might be polytypes, so we must instantiate and skolemise
-- Returns a wrapper of shape   ty_actual ~ ty_expected
tcSubType swap ctxt ty_actual ty_expected
  | isSigmaTy ty_actual
  = do { (sk_wrap, inst_wrap)
            <- tcGen ctxt ty_expected $ \ _ sk_rho -> do
            { (in_wrap, in_rho) <- deeplyInstantiate i_origin ty_actual
            ; cow <- unify in_rho sk_rho
            ; return (coToHsWrapper cow <.> in_wrap) }
       ; return (sk_wrap <.> inst_wrap) }

  | otherwise   -- Urgh!  It seems deeply weird to have equality
                -- when actual is not a polytype, and it makes a big
                -- difference e.g. tcfail104
  = do { cow <- unify ty_actual ty_expected
       ; return (coToHsWrapper cow) }
  where
    -- E.g., in the case of patterns and instance signatures,
    -- we call tcSubType with (expected, actual)
    -- rather than (actual, expected).   To get error messages the
    -- right way round we create the appropriate origin.
    unify  ty1 ty2 = uType (origin ty1 ty2) ty1 ty2
    origin ty1 ty2 =
      if isSwapped swap
        then TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 }
        else TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
    i_origin = origin ty_actual ty_expected

Being fine with the reported type errors, we still have a problem for the successful test.

{-# LANGUAGE InstanceSigs, TypeFamilies #-}

class C a where
  type T a
  m :: T a

instance C Int where
  type T Int = String

  -- The following type signature for m should be valid.
  m :: String
  m = "bla"

main :: IO ()
main = return ()

Running the test suite Core Lint complains about a type mismatch:

*** Core Lint errors : in result of Desugar (after optimization) ***
{-# LINE 15 "T9582.hs #-}: Warning:
    [RHS of $cm_amh :: Main.T GHC.Types.Int]
    The type of this binder doesn't match the type of its RHS: $cm_amh
    Binder's type: Main.T GHC.Types.Int
    Rhs type: [GHC.Types.Char]
*** Offending Program ***
$cm_amh :: Main.T GHC.Types.Int
[LclId, Str=DmdType]
$cm_amh = GHC.CString.unpackCString# "bla"#

Main.$fCInt [InlPrag=INLINE (sat-args=0)] :: Main.C GHC.Types.Int
[LclIdX[DFunId(nt)],
 Str=DmdType,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=False, ConLike=False,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=0,unsat_ok=False,boring_ok=True)
         Tmpl= $cm_amh
               `cast` (Sym (Main.NTCo:C[0] <GHC.Types.Int>_N)
                       :: Main.T GHC.Types.Int ~R# Main.C GHC.Types.Int)}]
Main.$fCInt =
  $cm_amh
  `cast` (Sym (Main.NTCo:C[0] <GHC.Types.Int>_N)
          :: Main.T GHC.Types.Int ~R# Main.C GHC.Types.Int)
...
*** End of Offense ***

Sounds like we cannot throw away the cast after all!? [The type synonym T Int = String does not seem to make it down to this level!?] We could return a cast from check_inst_sig. However, TcSigInfo which is produced by mkMethIds, does not provide for the storage of a coercion...

comment:10 Changed 5 years ago by thoughtpolice

Milestone: 7.10.1
Status: patchinfoneeded

Before we merge this, lets move it out of patch state until it's ready.

comment:11 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In e6a2050ebb6da316aecec66a6795715fbab355ca/ghc:

Fix the handling of instance signatures (Trac #9582, #9833)

This finally solves the issue of instance-method signatures that are
more polymorphic than the instanted class method.

See Note [Instance method signatures] in TcInstDcls.

A very nice fix for the two Trac tickets above.

comment:12 Changed 5 years ago by simonpj

Resolution: fixed
Status: infoneededclosed
Test Case: indexed-types/should_compile/T9582

I finally fixed this in a slightly different, more general way. Thank you for working on it; doing so clarified my thinking a lot.

Simon

comment:13 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In c34ef467429771edf0b2b18c05994c461c82df38/ghc:

Test Trac #7908

Fixed by e6a2050ebb6da316aecec66a6795715fbab355ca
along with #9582, #9833

comment:14 Changed 5 years ago by andreas.abel

Thanks for fixing. At the point where I was stuck, I would have needed to dive much deeper into GHC, I guess, and I did not have the time. It was an interesting experience anyway. Contributing to GHC is a full-time job, as for Agda, and I cannot work two jobs. I am rather glad to work on Agda, which "only" takes 15 min for compilation + test suite---as opposed to GHC's 120 min. Cheers and thanks for your work, Andreas

Note: See TracTickets for help on using tickets.