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/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

@@ -3,6 +3,7 @@ module Unify(Unify(..), matchList) where
 import Type
 import Subst
 import CType
+import Pred(expandSyn)
 import ErrorUtil(internalError)
 import Util(fastNub)
 
@@ -24,8 +25,15 @@ 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
+        | isATFAp t1' || isATFAp t2' = atfUnify bound_tyvars t1' t2'
+      where t1' = expandSynATF t1
+            t2' = expandSynATF t2
     mgu bound_tyvars t1 t2
         | kind t1 == KNum =
       case kind t2 of
@@ -42,6 +50,21 @@ instance Unify Type where
     mgu bound_tyvars (TCon tc1) (TCon tc2) | tc1==tc2 = Just (nullSubst, [])
     mgu bound_tyvars _ _ = Nothing
 
+-- Expand a saturated type-synonym application when (and only when) the
+-- expansion is a fully applied type-function (ATF) application, so that
+-- unification treats it exactly like the direct ATF application.
+-- Synonyms whose expansion does not reveal an ATF at the head are left
+-- unexpanded, because existing code relies on structural unification of
+-- unexpanded synonyms (e.g. synonyms that drop some of their parameters).
+expandSynATF :: Type -> Type
+expandSynATF t
+    | isSynAp t, not (isUnSatSyn t), isATFAp t' = t'
+    | otherwise = t
+  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

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected

@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_FieldSyn_Use_NoCtx.bs
+Error: "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 18, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    ExpSizeOf_FieldSyn_Use_NoCtx.Node a -> Prelude.Bool
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10

testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs

@@ -0,0 +1,15 @@
+package ExpSizeOf_FieldSyn_Use_WithCtx where
+
+-- As ExpSizeOf_FieldSyn_Use_NoCtx, but with the explicit Bits context that
+-- reading the field requires, so typecheck succeeds.  (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 :: (Bits a sa) => Node a -> Bool
+fnNeedsCtx n = n.wide == 0

testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs

@@ -0,0 +1,12 @@
+package ExpSizeOf_Let_NoCtx where
+
+-- A let binding whose type annotation contains SizeOf requires a Bits
+-- context: expanding the SizeOf in the declared type introduces an implicit
+-- Bits context, which must be provided by an explicit context on the
+-- enclosing definition.  Here none is given, so typecheck reports the
+-- missing context (T0030).  (GitHub Issue #890)
+
+foo :: a -> String
+foo _ = let x :: Bit (SizeOf a)
+            x = _
+        in  printType $ typeOf $ x

testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected

@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_Let_NoCtx.bs
+Error: "ExpSizeOf_Let_NoCtx.bs", line 9, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    a -> Prelude.String
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_Let_NoCtx.bs", line 10, column 22
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_Let_NoCtx.bs", line 10, column 22