[GHC] #9582: Associated Type Synonyms do not unfold in InstanceSigs

[GHC]

#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