Clean up Coercible handling, and interaction of data families with newtypes

This patch fixes Trac #9580, in which the Coercible machinery succeeded
even though the relevant data constructor was not in scope.

As usual I got dragged into a raft of refactoring changes,
all for the better.

* Delete TcEvidence.coercionToTcCoercion (now unused)

* Move instNewTyConTF_maybe, instNewTyCon_maybe to FamInst,
  and rename them to tcInstNewTyConTF_maybe, tcInstNewTyCon
  (They both return TcCoercions.)

* tcInstNewTyConTF_maybe also gets more convenient type,
  which improves TcInteract.getCoercibleInst

* Define FamInst.tcLookupDataFamInst, and use it in TcDeriv,
  (as well as in tcInstNewTyConTF_maybe)

* Improve error report for Coercible errors, when data familes
  are involved  Another use of tcLookupDataFamInst

* In TcExpr.tcTagToEnum, use tcLookupDataFamInst to replace
  local hacky code

* Fix Coercion.instNewTyCon_maybe and Type.newTyConInstRhs to deal
  with eta-reduced newtypes, using
  (new) Type.unwrapNewTyConEtad_maybe and (new) Type.applyTysX

Some small refactoring of TcSMonad.matchFam.

17 files changed, 220 insertions, 218 deletions

diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs
index 4b5bdb4d66..35de6a6bde 100644
--- a/compiler/hsSyn/HsUtils.lhs
+++ b/compiler/hsSyn/HsUtils.lhs
@@ -29,7 +29,7 @@ module HsUtils(
   mkHsPar, mkHsApp, mkHsConApp, mkSimpleHsAlt,
   mkSimpleMatch, unguardedGRHSs, unguardedRHS,
   mkMatchGroup, mkMatchGroupName, mkMatch, mkHsLam, mkHsIf,
-  mkHsWrap, mkLHsWrap, mkHsWrapCo, mkLHsWrapCo,
+  mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
   coToHsWrapper, mkHsDictLet, mkHsLams,
   mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo,
   mkLHsPar, mkHsCmdCast,
@@ -487,9 +487,14 @@ mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id
 mkHsWrap co_fn e | isIdHsWrapper co_fn = e
                  | otherwise           = HsWrap co_fn e
 
-mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id
+mkHsWrapCo :: TcCoercion   -- A Nominal coercion  a ~N b
+           -> HsExpr id -> HsExpr id
 mkHsWrapCo co e = mkHsWrap (coToHsWrapper co) e
 
+mkHsWrapCoR :: TcCoercion   -- A Representational coercion  a ~R b
+            -> HsExpr id -> HsExpr id
+mkHsWrapCoR co e = mkHsWrap (coToHsWrapperR co) e
+
 mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
 mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e)
 
@@ -497,10 +502,14 @@ mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id
 mkHsCmdCast co cmd | isTcReflCo co = cmd
                    | otherwise     = HsCmdCast co cmd
 
-coToHsWrapper :: TcCoercion -> HsWrapper
+coToHsWrapper :: TcCoercion -> HsWrapper   -- A Nominal coercion
 coToHsWrapper co | isTcReflCo co = idHsWrapper
                  | otherwise     = mkWpCast (mkTcSubCo co)
 
+coToHsWrapperR :: TcCoercion -> HsWrapper   -- A Representational coercion
+coToHsWrapperR co | isTcReflCo co = idHsWrapper
+                  | otherwise     = mkWpCast co
+
 mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
 mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
                        | otherwise           = CoPat co_fn p ty
diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs
index d0b2d0da5a..b917491af2 100644
--- a/compiler/typecheck/FamInst.lhs
+++ b/compiler/typecheck/FamInst.lhs
@@ -9,10 +9,11 @@ The @FamInst@ type: family instance heads
 --     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
 -- for details
 
-module FamInst ( 
+module FamInst (
+        FamInstEnvs, tcGetFamInstEnvs,
         checkFamInstConsistency, tcExtendLocalFamInstEnv,
-	tcLookupFamInst, 
-        tcGetFamInstEnvs,
+	tcLookupFamInst,
+        tcLookupDataFamInst, tcInstNewTyConTF_maybe, tcInstNewTyCon_maybe,
         newFamInst
     ) where
 
@@ -20,7 +21,9 @@ import HscTypes
 import FamInstEnv
 import InstEnv( roughMatchTcs )
 import Coercion( pprCoAxBranchHdr )
+import TcEvidence
 import LoadIface
+import Type( applyTysX )
 import TypeRep
 import TcRnMonad
 import TyCon
@@ -35,7 +38,6 @@ import Maybes
 import TcMType
 import TcType
 import Name
-import VarSet
 import Control.Monad
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -210,24 +212,60 @@ then we have a coercion (ie, type instance of family instance coercion)
 which implies that :R42T was declared as 'data instance T [a]'.
 
 \begin{code}
-tcLookupFamInst :: TyCon -> [Type] -> TcM (Maybe FamInstMatch)
-tcLookupFamInst tycon tys
+tcLookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe FamInstMatch
+tcLookupFamInst fam_envs tycon tys
   | not (isOpenFamilyTyCon tycon)
-  = return Nothing
+  = Nothing
   | otherwise
-  = do { instEnv <- tcGetFamInstEnvs
-       ; let mb_match = lookupFamInstEnv instEnv tycon tys 
-       ; traceTc "lookupFamInst" $
-         vcat [ ppr tycon <+> ppr tys
-              , pprTvBndrs (varSetElems (tyVarsOfTypes tys))
-              , ppr mb_match
-              -- , ppr instEnv
-         ]
-       ; case mb_match of
-	   [] -> return Nothing
-	   (match:_) 
-              -> return $ Just match
-       }
+  = case lookupFamInstEnv fam_envs tycon tys of
+      match : _ -> Just match
+      []        -> Nothing
+
+-- | If @co :: T ts ~ rep_ty@ then:
+--
+-- > instNewTyCon_maybe T ts = Just (rep_ty, co)
+--
+-- Checks for a newtype, and for being saturated
+-- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
+tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
+tcInstNewTyCon_maybe tc tys
+  | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc  -- Check for newtype
+  , tvs `leLength` tys                                    -- Check saturated enough
+  = Just (applyTysX tvs ty tys, mkTcUnbranchedAxInstCo Representational co_tc tys)
+  | otherwise
+  = Nothing
+
+tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
+                    -> (TyCon, [TcType], TcCoercion)
+-- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a)
+-- and returns a coercion between the two: co :: F [a] ~R FList a
+-- If there is no instance, or it's not a data family, just return
+-- Refl coercion and the original inputs
+tcLookupDataFamInst fam_inst_envs tc tc_args
+  | isDataFamilyTyCon tc
+  , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
+  , FamInstMatch { fim_instance = rep_fam
+                 , fim_tys      = rep_args } <- match
+  , let co_tc  = famInstAxiom rep_fam
+        rep_tc = dataFamInstRepTyCon rep_fam
+        co     = mkTcUnbranchedAxInstCo Representational co_tc rep_args
+  = (rep_tc, rep_args, co)
+
+  | otherwise
+  = (tc, tc_args, mkTcNomReflCo (mkTyConApp tc tc_args))
+
+tcInstNewTyConTF_maybe :: FamInstEnvs -> TcType -> Maybe (TyCon, TcType, TcCoercion)
+-- ^ If (instNewTyConTF_maybe envs ty) returns Just (ty', co)
+--   then co :: ty ~R ty'
+--        ty is (D tys) is a newtype (possibly after looking through the type family D)
+--        ty' is the RHS type of the of (D tys) newtype
+tcInstNewTyConTF_maybe fam_envs ty
+  | Just (tc, tc_args) <- tcSplitTyConApp_maybe ty
+  , let (rep_tc, rep_tc_args, fam_co) = tcLookupDataFamInst fam_envs tc tc_args
+  , Just (inner_ty, nt_co) <- tcInstNewTyCon_maybe rep_tc rep_tc_args
+  = Just (rep_tc, inner_ty, fam_co `mkTcTransCo` nt_co)
+  | otherwise
+  = Nothing
 \end{code}
 
 
diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index a14d29eee5..af05e80a08 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -888,9 +888,14 @@ mkEqnHelp overlap_mode tvs cls cls_tys tycon tc_args mtheta
            IsValid      -> mkOldTypeableEqn tvs cls tycon tc_args mtheta }
 
   | otherwise
-  = do { (rep_tc, rep_tc_args) <- lookup_data_fam tycon tc_args
-              -- Be careful to test rep_tc here: in the case of families,
-              -- we want to check the instance tycon, not the family tycon
+  = do {      -- Find the instance of a data family
+              -- Note [Looking up family instances for deriving]
+         fam_envs <- tcGetFamInstEnvs
+       ; let (rep_tc, rep_tc_args, _co) = tcLookupDataFamInst fam_envs tycon tc_args
+
+              -- If it's still a data family, the lookup failed; i.e no instance exists
+       ; when (isDataFamilyTyCon rep_tc)
+              (bale_out (ptext (sLit "No family instance for") <+> quotes (pprTypeApp tycon tc_args)))
 
        -- For standalone deriving (mtheta /= Nothing),
        -- check that all the data constructors are in scope.
@@ -923,23 +928,6 @@ mkEqnHelp overlap_mode tvs cls cls_tys tycon tc_args mtheta
                          tycon tc_args rep_tc rep_tc_args mtheta }
   where
      bale_out msg = failWithTc (derivingThingErr False cls cls_tys (mkTyConApp tycon tc_args) msg)
-
-     lookup_data_fam :: TyCon -> [Type] -> TcM (TyCon, [Type])
-     -- Find the instance of a data family
-     -- Note [Looking up family instances for deriving]
-     lookup_data_fam tycon tys
-       | not (isFamilyTyCon tycon)
-       = return (tycon, tys)
-       | otherwise
-       = ASSERT( isAlgTyCon tycon )
-         do { maybeFamInst <- tcLookupFamInst tycon tys
-            ; case maybeFamInst of
-                Nothing -> bale_out (ptext (sLit "No family instance for")
-                                     <+> quotes (pprTypeApp tycon tys))
-                Just (FamInstMatch { fim_instance = famInst
-                                   , fim_tys      = tys })
-                  -> let tycon' = dataFamInstRepTyCon famInst
-                     in return (tycon', tys) }
 \end{code}
 
 Note [Looking up family instances for deriving]
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index c8f3d06997..57f9829432 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -25,6 +25,7 @@ import Type
 import Kind ( isKind )
 import Unify            ( tcMatchTys )
 import Module
+import FamInst          ( FamInstEnvs, tcGetFamInstEnvs, tcLookupDataFamInst )
 import Inst
 import InstEnv
 import TyCon
@@ -983,18 +984,19 @@ Warn of loopy local equalities that were dropped.
 
 \begin{code}
 mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
-mkDictErr ctxt cts 
+mkDictErr ctxt cts
   = ASSERT( not (null cts) )
     do { inst_envs <- tcGetInstEnvs
+       ; fam_envs  <- tcGetFamInstEnvs
        ; lookups   <- mapM (lookup_cls_inst inst_envs) cts
        ; let (no_inst_cts, overlap_cts) = partition is_no_inst lookups
 
-       -- Report definite no-instance errors, 
+       -- Report definite no-instance errors,
        -- or (iff there are none) overlap errors
        -- But we report only one of them (hence 'head') because they all
        -- have the same source-location origin, to try avoid a cascade
        -- of error from one location
-       ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
+       ; (ctxt, err) <- mk_dict_err fam_envs ctxt (head (no_inst_cts ++ overlap_cts))
        ; mkErrorMsg ctxt ct1 err }
   where
     ct1:_ = elim_superclasses cts
@@ -1022,11 +1024,11 @@ mkDictErr ctxt cts
       where
         min_preds = mkMinimalBySCs (map ctPred cts)
 
-mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
+mk_dict_err :: FamInstEnvs -> ReportErrCtxt -> (Ct, ClsInstLookupResult)
             -> TcM (ReportErrCtxt, SDoc)
 -- Report an overlap error if this class constraint results
 -- from an overlap (returning Left clas), otherwise return (Right pred)
-mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell)) 
+mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) 
   | null matches  -- No matches but perhaps several unifiers
   = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct
        ; (ctxt, binds_msg) <- relevantBindings True ctxt ct
@@ -1190,11 +1192,13 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
           | (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2
           , not (t1 `eqType` t2)
           ]
-      | Just (tc,_) <- splitTyConApp_maybe ty1,
-        Just msg <- coercible_msg_for_tycon rdr_env tc
+      | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
+      , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
+      , Just msg <- coercible_msg_for_tycon rdr_env rep_tc
       = msg
-      | Just (tc,_) <- splitTyConApp_maybe ty2,
-        Just msg <- coercible_msg_for_tycon rdr_env tc
+      | Just (tc, tys) <- splitTyConApp_maybe ty2
+      , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
+      , Just msg <- coercible_msg_for_tycon rdr_env rep_tc
       = msg
       | otherwise
       = nest 2 $ sep [ ptext (sLit "because") <+> quotes (ppr ty1)
@@ -1203,26 +1207,17 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell))
       where
         (ty1, ty2) = getEqPredTys pred
 
-    dataConMissing rdr_env tc =
-        all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc))
-
     coercible_msg_for_tycon rdr_env tc
+        | isAbstractTyCon tc
+        = Just $ hsep [ ptext $ sLit "because the type constructor", quotes (pprSourceTyCon tc)
+                      , ptext $ sLit "is abstract" ]
         | isNewTyCon tc
-        = tyConAbstractMsg rdr_env tc empty
-        | otherwise
-        = Nothing
-
-    tyConAbstractMsg rdr_env tc occExpl
-        | isAbstractTyCon tc || dataConMissing rdr_env tc = Just $ vcat $
-            [ fsep [ ptext $ sLit "because the type constructor", quotes (ppr tc) <+> occExpl
-                   , ptext $ sLit "is abstract" ]
-            | isAbstractTyCon tc
-            ] ++
-            [ fsep [ ptext (sLit "because the constructor") <> plural (tyConDataCons tc)
-                   , ptext (sLit "of") <+> quotes (ppr tc) <+> occExpl
-                   , isOrAre (tyConDataCons tc) <+> ptext (sLit "not imported") ]
-            | dataConMissing rdr_env tc
-            ]
+        , [data_con] <- tyConDataCons tc
+        , let dc_name = dataConName data_con
+        , null (lookupGRE_Name rdr_env dc_name)
+        = Just $ hang (ptext (sLit "because the data constructor") <+> quotes (ppr dc_name))
+                    2 (sep [ ptext (sLit "of newtype") <+> quotes (pprSourceTyCon tc)
+                           , ptext (sLit "is not in scope") ])
         | otherwise = Nothing
 
 show_fixes :: [SDoc] -> SDoc
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index e2c2e60b04..8b64d2408b 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -28,14 +28,12 @@ module TcEvidence (
   mkTcAxiomRuleCo,
   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, 
   isTcReflCo, getTcCoVar_maybe,
-  tcCoercionRole, eqVarRole,
-  coercionToTcCoercion
+  tcCoercionRole, eqVarRole
   ) where
 #include "HsVersions.h"
 
 import Var
 import Coercion( LeftOrRight(..), pickLR, nthRole )
-import qualified Coercion as C
 import PprCore ()   -- Instance OutputableBndr TyVar
 import TypeRep  -- Knows type representation
 import TcType
@@ -95,8 +93,6 @@ differences
   * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter.
     This differs from the formalism, but corresponds to AxiomInstCo (see
     [Coercion axioms applied to coercions]).
-    Why can't we use [TcType] here, in code not relevant for the simplifier?
-    Because of coercionToTcCoercion.
 
 \begin{code}
 data TcCoercion 
@@ -425,21 +421,6 @@ ppr_forall_co p ty
     split1 tvs ty                 = (reverse tvs, ty)
 \end{code}
 
-Conversion from Coercion to TcCoercion
-(at the moment, this is only needed to convert the result of
-instNewTyConTF_maybe, so all unused cases are panics for now).
-
-\begin{code}
-coercionToTcCoercion :: C.Coercion -> TcCoercion
-coercionToTcCoercion = go
-  where
-    go (C.Refl r t)                = TcRefl r t
-    go (C.TransCo c1 c2)           = TcTransCo (go c1) (go c2)
-    go (C.AxiomInstCo coa ind cos) = TcAxiomInstCo coa ind (map go cos)
-    go (C.SubCo c)                 = TcSubCo (go c)
-    go (C.AppCo c1 c2)             = TcAppCo (go c1) (go c2)
-    go co                          = pprPanic "coercionToTcCoercion" (ppr co)
-\end{code}
 
 
 %************************************************************************
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 6188842b72..29020b4cb9 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -26,8 +26,7 @@ import TcUnify
 import BasicTypes
 import Inst
 import TcBinds
-import FamInst          ( tcLookupFamInst )
-import FamInstEnv       ( famInstAxiom, dataFamInstRepTyCon, FamInstMatch(..) )
+import FamInst          ( tcGetFamInstEnvs, tcLookupDataFamInst )
 import TcEnv
 import TcArrows
 import TcMatches
@@ -1225,49 +1224,32 @@ tcTagToEnum loc fun_name arg res_ty
         ; let mb_tc_app = tcSplitTyConApp_maybe ty'
               Just (tc, tc_args) = mb_tc_app
         ; checkTc (isJust mb_tc_app)
-                  (tagToEnumError ty' doc1)
+                  (mk_error ty' doc1)
 
         -- Look through any type family
-        ; (coi, rep_tc, rep_args) <- get_rep_ty ty' tc tc_args
+        ; fam_envs <- tcGetFamInstEnvs
+        ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args
+             -- coi :: tc tc_args ~ rep_tc rep_args
 
         ; checkTc (isEnumerationTyCon rep_tc)
-                  (tagToEnumError ty' doc2)
+                  (mk_error ty' doc2)
 
         ; arg' <- tcMonoExpr arg intPrimTy
         ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun))
               rep_ty = mkTyConApp rep_tc rep_args
 
-        ; return (mkHsWrapCo coi $ HsApp fun' arg') }
+        ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') }
+                  -- coi is a Representational coercion
   where
     doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
                 , ptext (sLit "e.g. (tagToEnum# x) :: Bool") ]
     doc2 = ptext (sLit "Result type must be an enumeration type")
-    doc3 = ptext (sLit "No family instance for this type")
-
-    get_rep_ty :: TcType -> TyCon -> [TcType]
-               -> TcM (TcCoercion, TyCon, [TcType])
-        -- Converts a family type (eg F [a]) to its rep type (eg FList a)
-        -- and returns a coercion between the two
-    get_rep_ty ty tc tc_args
-      | not (isFamilyTyCon tc)
-      = return (mkTcNomReflCo ty, tc, tc_args)
-      | otherwise
-      = do { mb_fam <- tcLookupFamInst tc tc_args
-           ; case mb_fam of
-               Nothing -> failWithTc (tagToEnumError ty doc3)
-               Just (FamInstMatch { fim_instance = rep_fam
-                                  , fim_tys      = rep_args })
-                   -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo Nominal co_tc rep_args)
-                             , rep_tc, rep_args )
-                 where
-                   co_tc  = famInstAxiom rep_fam
-                   rep_tc = dataFamInstRepTyCon rep_fam }
-
-tagToEnumError :: TcType -> SDoc -> SDoc
-tagToEnumError ty what
-  = hang (ptext (sLit "Bad call to tagToEnum#")
-           <+> ptext (sLit "at type") <+> ppr ty)
-         2 what
+
+    mk_error :: TcType -> SDoc -> SDoc
+    mk_error ty what
+      = hang (ptext (sLit "Bad call to tagToEnum#")
+               <+> ptext (sLit "at type") <+> ppr ty)
+           2 what
 \end{code}
 
 
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 33249f4b04..e56c96131f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -28,7 +28,7 @@ import Name
 import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
                  is_decl, Provenance(Imported), gre_prov )
 import FunDeps
-import FamInstEnv ( FamInstEnvs, instNewTyConTF_maybe )
+import FamInst
 
 import TcEvidence
 import Outputable
@@ -1820,29 +1820,27 @@ matchClassInst _ clas [ ty ] _
      String    -> SSymbol n
      SSymbol n -> KnownSymbol n
   -}
-  makeDict evLit =
-    case unwrapNewTyCon_maybe (classTyCon clas) of
-      Just (_,_, axDict)
-        | [ meth ]   <- classMethods clas
-        , Just tcRep <- tyConAppTyCon_maybe -- SNat
+  makeDict evLit
+    | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
+    , [ meth ]   <- classMethods clas
+    , Just tcRep <- tyConAppTyCon_maybe -- SNat
                       $ funResultTy         -- SNat n
                       $ dropForAlls         -- KnownNat n => SNat n
                       $ idType meth         -- forall n. KnownNat n => SNat n
-        , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
-        -> return $
-           let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axRep  [ty]
-               co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axDict [ty]
-           in GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co1 co2)
+    , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
+    = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co_dict co_rep))
 
-      _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
+    | otherwise
+    = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
 
 matchClassInst _ clas [ _k, ty1, ty2 ] loc
-  | clas == coercibleClass =  do
-      traceTcS "matchClassInst for" $ quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc)
-      ev <- getCoercibleInst loc ty1 ty2
-      traceTcS "matchClassInst returned" $ ppr ev
-      return ev
+  | clas == coercibleClass
+  = do { traceTcS "matchClassInst for" $
+         quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc)
+       ; ev <- getCoercibleInst loc ty1 ty2
+       ; traceTcS "matchClassInst returned" $ ppr ev
+       ; return ev }
 
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
@@ -1927,11 +1925,11 @@ matchClassInst inerts clas tys loc
 -- See Note [Coercible Instances]
 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
 getCoercibleInst :: CtLoc -> TcType -> TcType -> TcS LookupInstResult
-getCoercibleInst loc ty1 ty2 = do
-      -- Get some global stuff in scope, for nice pattern-guard based code in `go`
-      rdr_env <- getGlobalRdrEnvTcS
-      famenv <- getFamInstEnvs
-      go famenv rdr_env
+getCoercibleInst loc ty1 ty2
+  = do { -- Get some global stuff in scope, for nice pattern-guard based code in `go`
+         rdr_env <- getGlobalRdrEnvTcS
+       ; famenv <- getFamInstEnvs
+       ; go famenv rdr_env }
   where
   go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
   go famenv rdr_env
@@ -1939,8 +1937,8 @@ getCoercibleInst loc ty1 ty2 = do
 
     -- Coercible a a                             (see case 1 in [Coercible Instances])
     | ty1 `tcEqType` ty2
-    = do return $ GenInst []
-                $ EvCoercion (TcRefl Representational ty1)
+    = return $ GenInst []
+             $ EvCoercion (TcRefl Representational ty1)
 
     -- Coercible (forall a. ty) (forall a. ty')  (see case 2 in [Coercible Instances])
     | tcIsForAllTy ty1
@@ -1948,33 +1946,29 @@ getCoercibleInst loc ty1 ty2 = do
     , let (tvs1,body1) = tcSplitForAllTys ty1
           (tvs2,body2) = tcSplitForAllTys ty2
     , equalLength tvs1 tvs2
-    = do
-       ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
-       return $ GenInst [] ev_term
+    = do { ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
+         ; return $ GenInst [] ev_term }
 
     -- Coercible NT a                            (see case 3 in [Coercible Instances])
-    | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
-      Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
-      dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
-    = do markDataConsAsUsed rdr_env tc
-         ct_ev <- requestCoercible loc concTy ty2
-         local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2
-         let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
-             tcCo = TcLetCo binds $
-                            coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var
-         return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
+    | Just (rep_tc, concTy, ntCo) <- tcInstNewTyConTF_maybe famenv ty1
+    , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
+    = do { markDataConsAsUsed rdr_env rep_tc
+         ; ct_ev <- requestCoercible loc concTy ty2
+         ; local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2
+         ; let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
+               tcCo = TcLetCo binds (ntCo `mkTcTransCo` mkTcCoVarCo local_var)
+         ; return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) }
 
     -- Coercible a NT                            (see case 3 in [Coercible Instances])
-    | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
-      Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
-      dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
-    = do markDataConsAsUsed rdr_env tc
-         ct_ev <- requestCoercible loc ty1 concTy
-         local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ty1 concTy
-         let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
-             tcCo = TcLetCo binds $
-                            mkTcCoVarCo local_var `mkTcTransCo` mkTcSymCo (coercionToTcCoercion ntCo)
-         return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
+    | Just (rep_tc, concTy, ntCo) <- tcInstNewTyConTF_maybe famenv ty2
+    , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
+    = do { markDataConsAsUsed rdr_env rep_tc
+         ; ct_ev <- requestCoercible loc ty1 concTy
+         ; local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ty1 concTy
+         ; let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev)))
+               tcCo = TcLetCo binds $
+                         mkTcCoVarCo local_var `mkTcTransCo` mkTcSymCo ntCo
+         ; return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) }
 
     -- Coercible (D ty1 ty2) (D ty1' ty2')       (see case 4 in [Coercible Instances])
     | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 9891f77795..4cb679d49b 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -86,7 +86,7 @@ module TcSMonad (
 
     getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
 
-    matchFam, matchOpenFam,
+    matchFam, 
     checkWellStagedDFun,
     pprEq                                    -- Smaller utils, re-exported from TcM
                                              -- TODO (DV): these are only really used in the
@@ -122,6 +122,7 @@ import Name
 import RdrName (RdrName, GlobalRdrEnv)
 import RnEnv (addUsedRdrNames)
 import Var
+import VarSet
 import VarEnv
 import Outputable
 import Bag
@@ -145,7 +146,6 @@ import Data.IORef
 import Data.List( partition )
 
 #ifdef DEBUG
-import VarSet
 import Digraph
 #endif
 \end{code}
@@ -1863,20 +1863,21 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
   where
     new_pred = mkTcEqPred nlhs nrhs
 
-maybeSym :: SwapFlag -> TcCoercion -> TcCoercion 
+maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
 maybeSym IsSwapped  co = mkTcSymCo co
 maybeSym NotSwapped co = co
 
-
-matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch)
-matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args
-
 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
 matchFam tycon args
   | isOpenSynFamilyTyCon tycon
-  = do { maybe_match <- matchOpenFam tycon args
-       ; case maybe_match of
+  = do { fam_envs <- getFamInstEnvs
+       ; let mb_match = tcLookupFamInst fam_envs tycon args
+       ; traceTcS "lookupFamInst" $
+                  vcat [ ppr tycon <+> ppr args
+                       , pprTvBndrs (varSetElems (tyVarsOfTypes args))
+                       , ppr mb_match ]
+       ; case mb_match of
            Nothing -> return Nothing
            Just (FamInstMatch { fim_instance = famInst
                               , fim_tys      = inst_tys })
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index f0c0516c0e..fc6c8a7669 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -1228,9 +1228,9 @@ mkCoCast c g
 -- Checks for a newtype, and for being saturated
 instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
 instNewTyCon_maybe tc tys
-  | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc  -- Check for newtype
-  , tys `lengthIs` tyConArity tc                      -- Check saturated
-  = Just (substTyWith tvs tys ty, mkUnbranchedAxInstCo Representational co_tc tys)
+  | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc  -- Check for newtype
+  , tvs `leLength` tys                                    -- Check saturated enough
+  = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys)
   | otherwise
   = Nothing
 
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index 1308984f4f..3ff9e3be7c 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -23,11 +23,10 @@ module FamInstEnv (
 
         FamInstMatch(..),
         lookupFamInstEnv, lookupFamInstEnvConflicts,
-
-        isDominatedBy,
+        chooseBranch, isDominatedBy,
 
         -- Normalisation
-        instNewTyConTF_maybe, chooseBranch, topNormaliseType, topNormaliseType_maybe,
+        topNormaliseType, topNormaliseType_maybe,
         normaliseType, normaliseTcApp,
 
         -- Flattening
@@ -863,7 +862,6 @@ findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = inc
 
 -- fail if no branches left
 findBranch [] _ _ = Nothing
-
 \end{code}
 
 
@@ -874,29 +872,6 @@ findBranch [] _ _ = Nothing
 %************************************************************************
 
 \begin{code}
--- | Unwrap a newtype of a newtype intances. This is analogous to
---   Coercion.instNewTyCon_maybe; differences are:
---     * it also lookups up newtypes families, and
---     * it does not require the newtype to be saturated.
---       (a requirement using it for Coercible)
-instNewTyConTF_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type, Coercion)
-instNewTyConTF_maybe env tc tys = result
-  where
-  (co1, tc2, tys2)
-    | Just (co, rhs1) <- reduceTyFamApp_maybe env Representational tc tys
-    , Just (tc2, tys2) <- splitTyConApp_maybe rhs1
-    = (co, tc2, tys2)
-    | otherwise
-    = (mkReflCo Representational (mkTyConApp tc tys), tc, tys)
-
-  result
-     | Just (_, _, co_tc) <- unwrapNewTyCon_maybe tc2 -- Check for newtype
-     , newTyConEtadArity tc2 <= length tys2           -- Check for enough arguments
-     = Just (newTyConInstRhs tc2 tys2
-            , co1 `mkTransCo` mkUnbranchedAxInstCo Representational co_tc tys2)
-     | otherwise
-     = Nothing
-
 topNormaliseType :: FamInstEnvs -> Type -> Type
 topNormaliseType env ty = case topNormaliseType_maybe env ty of
                             Just (_co, ty') -> ty'
@@ -963,7 +938,7 @@ normaliseTcApp env role tc tys
                 -- we do not do anything
   = let (co, ntys) = normaliseTcArgs env role tc tys in
     (co, mkTyConApp tc ntys)
-    
+
 
 ---------------
 normaliseTcArgs :: FamInstEnvs            -- environment with family instances
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 65b5645d74..64a2a6cc3c 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -73,7 +73,8 @@ module TyCon(
         synTyConDefn_maybe, synTyConRhs_maybe, 
         tyConExtName,           -- External name for foreign types
         algTyConRhs,
-        newTyConRhs, newTyConEtadArity, newTyConEtadRhs, unwrapNewTyCon_maybe,
+        newTyConRhs, newTyConEtadArity, newTyConEtadRhs, 
+        unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
         tupleTyConBoxity, tupleTyConSort, tupleTyConArity,
 
         -- ** Manipulating TyCons
@@ -1170,6 +1171,12 @@ unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs,
                            = Just (tvs, rhs, co)
 unwrapNewTyCon_maybe _     = Nothing
 
+unwrapNewTyConEtad_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
+unwrapNewTyConEtad_maybe (AlgTyCon { algTcRhs = NewTyCon { nt_co = co,
+                                                           nt_etad_rhs = (tvs,rhs) }})
+                           = Just (tvs, rhs, co)
+unwrapNewTyConEtad_maybe _ = Nothing
+
 isProductTyCon :: TyCon -> Bool
 -- True of datatypes or newtypes that have
 --   one, vanilla, data constructor
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 6c59450aa6..94e8c24277 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -36,7 +36,7 @@ module Type (
 
         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
         mkPiKinds, mkPiType, mkPiTypes,
-        applyTy, applyTys, applyTysD, dropForAlls,
+        applyTy, applyTys, applyTysD, applyTysX, dropForAlls,
 
         mkNumLitTy, isNumLitTy,
         mkStrLitTy, isStrLitTy,
@@ -575,11 +575,10 @@ newTyConInstRhs :: TyCon -> [Type] -> Type
 -- arguments, using an eta-reduced version of the @newtype@ if possible.
 -- This requires tys to have at least @newTyConInstArity tycon@ elements.
 newTyConInstRhs tycon tys
-    = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
-      mkAppTys (substTyWith tvs tys1 ty) tys2
+    = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs )
+      applyTysX tvs rhs tys
   where
-    (tvs, ty)    = newTyConEtadRhs tycon
-    (tys1, tys2) = splitAtList tvs tys
+    (tvs, rhs) = newTyConEtadRhs tycon
 \end{code}
 
 
@@ -824,13 +823,22 @@ applyTysD doc orig_fun_ty arg_tys
   = substTyWith (take n_args tvs) arg_tys
                 (mkForAllTys (drop n_args tvs) rho_ty)
   | otherwise           -- Too many type args
-  = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty )        -- Zero case gives infinite loop!
+  = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys )        -- Zero case gives infinite loop!
     applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty)
                   (drop n_tvs arg_tys)
   where
     (tvs, rho_ty) = splitForAllTys orig_fun_ty
-    n_tvs = length tvs
+    n_tvs  = length tvs
     n_args = length arg_tys
+
+applyTysX :: [TyVar] -> Type -> [Type] -> Type
+-- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
+applyTysX tvs body_ty arg_tys
+  = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
+    mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
+             (drop n_tvs arg_tys)
+  where
+    n_tvs = length tvs
 \end{code}
 
 
diff --git a/testsuite/tests/indexed-types/should_fail/T9580.hs b/testsuite/tests/indexed-types/should_fail/T9580.hs
new file mode 100644
index 0000000000..de5455f493
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T9580.hs
@@ -0,0 +1,7 @@
+module T9580 where
+
+import T9580a
+import Data.Coerce
+
+foo :: Dimensional Int Double -> Double
+foo x = coerce x
diff --git a/testsuite/tests/indexed-types/should_fail/T9580.stderr b/testsuite/tests/indexed-types/should_fail/T9580.stderr
new file mode 100644
index 0000000000..19ceefb0ff
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T9580.stderr
@@ -0,0 +1,10 @@
+[1 of 2] Compiling T9580a           ( T9580a.hs, T9580a.o )
+[2 of 2] Compiling T9580            ( T9580.hs, T9580.o )
+
+T9580.hs:7:9:
+    Could not coerce from ‘Dimensional Int Double’ to ‘Double’
+    because the data constructor ‘T9580a.Quantity'’
+      of newtype ‘Dimensional Int v’ is not in scope
+      arising from a use of ‘coerce’
+    In the expression: coerce x
+    In an equation for ‘foo’: foo x = coerce x
diff --git a/testsuite/tests/indexed-types/should_fail/T9580a.hs b/testsuite/tests/indexed-types/should_fail/T9580a.hs
new file mode 100644
index 0000000000..578c8bafb8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T9580a.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE KindSignatures, TypeFamilies #-}
+module T9580a( Dimensional ) where
+
+data family Dimensional var :: * -> *
+newtype instance Dimensional Int v = Quantity' v
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 2862f1e854..f06060efd0 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -128,4 +128,5 @@ test('T9357', normal, compile_fail, [''])
 test('T9371', normal, compile_fail, [''])
 test('T9433', normal, compile_fail, [''])
 test('BadSock', normal, compile_fail, [''])
+test('T9580', normal, multimod_compile_fail, ['T9580', ''])
 
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index 5bb9210a13..b95b4cea67 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -33,7 +33,8 @@ TcCoercibleFail.hs:16:8:
 
 TcCoercibleFail.hs:18:8:
     Could not coerce from ‘Int’ to ‘Down Int’
-    because the constructor of ‘Down’ is not imported
+    because the data constructor ‘Data.Ord.Down’
+      of newtype ‘Down’ is not in scope
       arising from a use of ‘coerce’
     In the expression: coerce
     In the expression: coerce $ one :: Down Int