Fix spurious T0029 when a field reaches an ATF through a type synonym

src/comp/CtxRed.hs

@@ -385,12 +385,16 @@ ctxRedCQType' isInstHead cqt = do
     -- (and do it here, after "convCQType", so that "expTFun" sees
     -- the qualified types)
     (qs, t) <- if isInstHead
-               then do -- XXX disable expanding of type synonyms until
-                       -- XXX failures with TLM instances are resolved
-                       -- XXX (vqs_extra, t1) <- expTFun t0 (expandSyn t0)
-                       (vqs_extra, t1) <- expTFun t0
+               then do (vqs_extra, t1) <- expTFun (expandSyn t0)
                        let qs_extra = map toPredWithPositions vqs_extra
-                       return (qs0 ++ qs_extra, t1)
+                       -- Use the expanded type t1 only if expTFun actually
+                       -- found something to expand (i.e. generated predicates).
+                       -- Otherwise keep the original t0.
+                       -- XXX we should probably be unconditionally expanding synonymns
+                       -- here and in tiField1, but there is existing code that relies on
+                       -- the current behavior, so changing this requires more thought.
+                       let t' = if null vqs_extra then t0 else t1
+                       return (qs0 ++ qs_extra, t')
                else return (qs0, t0)
 
     -- construct the predicates and try to reduce them

src/comp/MakeSymTab.hs

@@ -464,10 +464,39 @@ checkNoTypeFunInHead errh r mi clsId args =
             | otherwise = []
         findTypeFun (TAp f a) = findTypeFun f ++ findTypeFun a
         findTypeFun _ = []
+        -- A type function can also be hidden behind a type synonym.
+        -- Expand each saturated synonym application and reject any type
+        -- function application in it that mentions a type variable (or
+        -- is not fully applied): such an application can neither be
+        -- reduced away nor used for instance matching.  Ground
+        -- applications are left alone; context reduction expands and
+        -- reduces them to a concrete type (Bug 1729, GitHub issue #311;
+        -- see ExpSizeOf_InstancesBaseSyn in the testsuite).  The error
+        -- is reported at the position of the synonym use.
+        synArity i | Just (TypeInfo { ti_sort = TItype n _ }) <- findType r i = Just n
+                   | otherwise = Nothing
+        findSynTypeFun t =
+            case splitTAp t of
+              (TCon (TyCon i _ _), as)
+                | Just n <- synArity i, toInteger (length as) >= n ->
+                    [ (getPosition i, tf)
+                    | tf <- varTypeFuns (expandSyn (updTypes r t)) ]
+              (_, as) -> concatMap findSynTypeFun as
+        varTypeFuns t =
+            case splitTAp t of
+              (TCon (TyCon i _ (TIatf { atf_param_idxs = pIdxs })), as)
+                | length as /= length pIdxs || not (null (tv as)) ->
+                    i : concatMap varTypeFuns as
+              (_, as) -> concatMap varTypeFuns as
         -- Only check non-determined positions
         nonDetArgs = [ arg | (idx, arg) <- zip [0..] args
                      , not (S.member idx determinedIdxs) ]
-        found = concatMap findTypeFun nonDetArgs
+        -- Report both the directly-written type functions and the ones
+        -- hidden behind synonyms, deduplicated (a directly-written type
+        -- function inside a synonym's argument can also appear in the
+        -- synonym's expansion).
+        checkArg a = nub (findTypeFun a ++ findSynTypeFun a)
+        found = concatMap checkArg nonDetArgs
     in if null found then ()
        else bsErrorUnsafe errh
                 [ (pos, EATFInInstanceHead (pfpString tfId))

src/comp/TCheck.hs

@@ -2394,7 +2394,14 @@ tiExpl''' as0 i sc alts me (oqt@(oqs :=> ot), vts) = do
 
     -- type functions like SizeOf could have crept into the predicates
     -- via unification, so we expand them out so that they can be satisfied
-    ps <- concatMapM (expTConPred . expandSynVPred) ps0
+    ps1 <- concatMapM (expTConPred . expandSynVPred) ps0
+
+    -- Expand type synonyms and type functions in the declared type to generate
+    -- implicit class predicates (e.g. SizeOf a generates Bits a n).
+    s_ot <- getSubst
+    let ot_expanded = expandSyn (apSub s_ot ot)
+    (ot_ps, _) <- expTFun ot_expanded
+    let ps = ps1 ++ ot_ps
 
     satTraceM ("tiExpl " ++ ppReadable i ++ " ps: " ++ ppReadable ps)
 

src/comp/Unify.hs

@@ -1,8 +1,10 @@
 {-# LANGUAGE PatternGuards #-}
 module Unify(Unify(..), matchList) where
+import Data.Maybe(fromMaybe, isJust)
 import Type
 import Subst
 import CType
+import Pred(expandSyn)
 import ErrorUtil(internalError)
 import Util(fastNub)
 
@@ -24,8 +26,16 @@ class Unify t where
 instance Unify Type where
     -- an unreducable ATF application: identical types unify cleanly (reflexivity);
     -- different types generate a deferred equality constraint.
+    -- A type synonym is expanded when (and only when) that exposes an ATF
+    -- application, so that a synonym-hidden ATF unifies exactly like the
+    -- direct ATF application, instead of a variable being structurally
+    -- bound to the unexpanded synonym (which pins a fundep-determined
+    -- variable and makes derived-instance schemes spuriously mismatch).
     mgu bound_tyvars t1 t2
-        | isATFAp t1 || isATFAp t2 = atfUnify bound_tyvars t1 t2
+        | isJust m1 || isJust m2 =
+            atfUnify bound_tyvars (fromMaybe t1 m1) (fromMaybe t2 m2)
+      where m1 = asATFAp t1
+            m2 = asATFAp t2
     mgu bound_tyvars t1 t2
         | kind t1 == KNum =
       case kind t2 of
@@ -42,6 +52,27 @@ instance Unify Type where
     mgu bound_tyvars (TCon tc1) (TCon tc2) | tc1==tc2 = Just (nullSubst, [])
     mgu bound_tyvars _ _ = Nothing
 
+-- Return the type as a fully applied type-function (ATF) application,
+-- if it is one -- either directly, or behind a saturated type synonym.
+-- Synonyms are not expanded unconditionally, for three reasons:
+--  * unification is a hot path and expandSyn is a deep expansion, so
+--    only synonym-headed types should pay for it;
+--  * expandSyn fails on unsaturated synonym applications, so saturation
+--    must be checked first; and
+--  * a synonym whose expansion is not an ATF application must keep the
+--    existing structural unification of the unexpanded synonym, which
+--    existing code relies on (e.g. synonyms that drop some of their
+--    parameters; see GitHub issue #311).
+asATFAp :: Type -> Maybe Type
+asATFAp t
+    | isATFAp t = Just t
+    | isSynAp t, not (isUnSatSyn t), isATFAp t' = Just t'
+    | otherwise = Nothing
+  where t' = expandSyn t
+        isSynAp tt = case fst (splitTAp tt) of
+                       TCon (TyCon _ _ (TItype _ _)) -> True
+                       _ -> False
+
 atfUnify :: [TyVar] -> Type -> Type -> Maybe (Subst, [(Type, Type)])
 atfUnify bound_tyvars t1 t2
     | t1 == t2 = Just (nullSubst, [])

testsuite/bsc.typechecker/primtcons/CExtendATF.bsv

@@ -0,0 +1,64 @@
+// A variant of CExtendSynonym that puts a type function (here a user-defined
+// ATF, 'IdW') into the id-type synonyms, so that expanding the synonyms in the
+// instance head *does* reveal a type function.  That forces the conditional
+// synonym expansion in 'CtxRed.ctxRedCQType'' to fire (unlike CExtendSynonym,
+// where the plain synonyms are left unexpanded), which re-introduces the
+// dangling 'addr_size' parameter and makes typecheck fail with T0035.
+//
+// This is the case that is *still broken* -- see the XXX in ctxRedCQType' and
+// GitHub Issue #311 (and bsc-contrib PR 46, which worked around the analogous
+// AMBA_TLM failure by adding explicit method types).  CExtendATFExplicit.bsv
+// shows that adding explicit types makes it compile, which suggests the
+// problem is one of inference ordering rather than anything fundamental.
+// The same failure occurs with the builtin type function SizeOf in place of
+// the ATF 'IdW'.
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+   let out = unpack(zExtend(pack(value)));
+   return out;
+endfunction
+
+// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf).
+typeclass HasIdW#(type t, numeric type n) dependencies (t determines n);
+   type IdW#(type t) = n;
+endtypeclass
+
+instance HasIdW#(Bit#(n), n);
+endinstance
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(IdW#(Bit#(id_size)))  TLMId#(`TLM_PRM_DCL);
+typedef Bit#(IdW#(Bit#(id_size)))  AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function getId(payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance

testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv

@@ -0,0 +1,55 @@
+// As CExtendATF.bsv, but with an explicit type on the 'getId' method.  With
+// the explicit type, typecheck succeeds despite the ATF-triggered synonym
+// expansion in the instance head.  This is the workaround used in bsc-contrib
+// PR 46, and it shows that the CExtendATF failure is not fundamental (see the
+// XXX in CtxRed.ctxRedCQType' and GitHub Issue #311).
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+   let out = unpack(zExtend(pack(value)));
+   return out;
+endfunction
+
+// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf).
+typeclass HasIdW#(type t, numeric type n) dependencies (t determines n);
+   type IdW#(type t) = n;
+endtypeclass
+
+instance HasIdW#(Bit#(n), n);
+endinstance
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(IdW#(Bit#(id_size)))  TLMId#(`TLM_PRM_DCL);
+typedef Bit#(IdW#(Bit#(id_size)))  AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function TLMId#(`TLM_PRM) getId(AxiAddrCmd#(`TLM_PRM) payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance

testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv

@@ -0,0 +1,55 @@
+// Reduced version of the bsc-contrib AMBA_TLM library (see bsc-contrib PR 46).
+// Check that we can use type synonyms in instance heads.  The synonyms 'TLMId'
+// and 'AxiId' drop the 'addr_size' parameter; expanding them fully in the
+// instance head would leave 'addr_size' dangling and break unification.  This
+// exercises the (now conditional) synonym expansion in CtxRed.ctxRedCQType' --
+// see the XXX there and GitHub Issue #311.  Because these synonyms contain no
+// type function, the conditional expansion leaves them alone, so this compiles;
+// bsc-contrib PR 46 added explicit method types to work around the earlier
+// (unconditional-expansion) failure, and those are no longer needed here.
+// CExtendATF.bsv shows a variant that *does* still fail, because it puts a type
+// function in the synonyms and so triggers the expansion.
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+
+   let out = unpack(zExtend(pack(value)));
+
+   return out;
+endfunction
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(id_size)     TLMId#(`TLM_PRM_DCL);
+typedef Bit#(id_size)     AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function getId(payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs

@@ -0,0 +1,20 @@
+package ExpSizeOf_FieldSyn_BS where
+
+-- Classic syntax version of ExpSizeOf_FieldSyn.
+-- A struct with a field whose type uses SizeOf through a synonym chain.
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct Node dataType =
+  dat    :: dataType
+  unused :: T dataType
+ deriving (Bits, Eq)
+
+{-# synthesize sysExpSizeOf_FieldSyn_BS #-}
+sysExpSizeOf_FieldSyn_BS :: Module Empty
+sysExpSizeOf_FieldSyn_BS = module
+  r_node :: Reg (Node (UInt 3)) <- mkRegU
+  r_data :: Reg (UInt 3)        <- mkRegU
+  rules
+    when True ==> r_data := r_node.dat

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs

@@ -0,0 +1,12 @@
+package ExpSizeOf_FieldSyn_Minimal where
+
+-- Minimal reproduction: a struct with a field type that uses SizeOf
+-- through a type synonym.  Without expanding synonyms in ctxRedCQType, the
+-- needed Bits context is not injected into the derived Generic instance, and
+-- that instance then fails to typecheck -- i.e. the failure is a compile
+-- error, so compile_pass is a sufficient regression guard here.
+
+type S t = SizeOf t
+
+struct Foo a =
+  x :: Bit (S a)

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs

@@ -0,0 +1,15 @@
+package ExpSizeOf_FieldSyn_Unbound_NoCtx where
+
+-- A struct field whose type uses SizeOf through a synonym, where the type
+-- variable is *not* a parameter of the struct.  Because the variable is
+-- unbound in the struct type, the field's implicit Bits context cannot be
+-- satisfied by the struct itself, so the field must declare it explicitly.
+-- Here it does not, so typecheck reports the missing context (T0030).
+-- (GitHub Issues #890 and #310: the field's context requirement is not
+-- wrongly exempted here, despite the XXX in TCheck.tiField1.)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct MyS =
+  sfield :: T dataType

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs

@@ -0,0 +1,11 @@
+package ExpSizeOf_FieldSyn_Unbound_WithCtx where
+
+-- As ExpSizeOf_FieldSyn_Unbound_NoCtx, but the field declares the Bits
+-- context that its SizeOf-using type requires, so typecheck succeeds.
+-- (GitHub Issues #890 and #310)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct MyS =
+  sfield :: (Bits dataType sz) => T dataType

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs

@@ -0,0 +1,19 @@
+package ExpSizeOf_FieldSyn_Use_NoCtx where
+
+-- Reading a struct field whose type uses SizeOf through a synonym chain
+-- requires a Bits context on the struct's type parameter.  The field type
+-- 'T a' expands to 'UInt (SizeOf a)', and reading the field during typecheck
+-- introduces the implicit 'Bits a' context.  Here it is not provided, so
+-- typecheck reports the missing context (T0030), confirming that the field's
+-- context requirement is handled during typecheck.  (GitHub Issue #890)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct Node dataType =
+  dat  :: dataType
+  wide :: T dataType
+ deriving (Bits, Eq)
+
+fnNeedsCtx :: Node a -> Bool
+fnNeedsCtx n = n.wide == 0