#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by andreas.abel): Relevant snippet: Checking InstanceSigs uses eqType. https://github.com/ghc/ghc/blob/master/compiler/typecheck/TcInstDcls.lhs {{{#!hs -- 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 {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: new Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by andreas.abel): Thanks, Simon, I got quite far with your help: {{{#!hs -- 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: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: patch Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => patch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: patch Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by andreas.abel): Thanks for the help! Now I use PatSigOrigin to swap expected/actual type in the error message generated by tcSubType. {{{#!hs -- 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, {{{#!hs 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: {{{#!hs 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? {{{#!hs TypeEqOrigin{} -> u_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/29a2f93a26f714b79a59617d20b73b2e16... some cleaning needed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: patch Type: bug | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (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/e43d6f1f90f8d395fb21696c5f8a1641a7... 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... {{{#!hs 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. {{{#!hs {-# 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] _N) :: Main.T GHC.Types.Int ~R# Main.C GHC.Types.Int)}] Main.$fCInt = $cm_amh `cast` (Sym (Main.NTCo:C[0] _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... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: infoneeded Type: bug | Milestone: 7.10.1 Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"e6a2050ebb6da316aecec66a6795715fbab355ca/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="e6a2050ebb6da316aecec66a6795715fbab355ca" 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. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9582: Associated Type Synonyms do not unfold in InstanceSigs -------------------------------------+------------------------------------- Reporter: | Owner: andreas.abel | Status: closed Type: bug | Milestone: 7.10.1 Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: InstanceSigs (Type checker) | TypeFamilies Resolution: fixed | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: indexed- | types/should_compile/T9582 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"c34ef467429771edf0b2b18c05994c461c82df38/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="c34ef467429771edf0b2b18c05994c461c82df38" Test Trac #7908 Fixed by e6a2050ebb6da316aecec66a6795715fbab355ca along with #9582, #9833 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9582#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler